CESAR
Specification and verification of concurrent systems in CESAR. The aim of this paper is to illustrate by an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications. CESAR allows the progressive validation of the algorithmic description of a system of communicating sequential processes with respect to a given set of specifications. The algorithmic description is done in a high level language inspired from CSP and specifications are a set of formulas of a branching time logic, the temporal operators of which can be computed iteratively as fixed points of monotonic predicate transformers. The verification of a system consists in obtaining by automatic translation of its description program an Interpreted Petri Net representing it and evaluating each formula of the specifications.
Keywords for this software
References in zbMATH (referenced in 131 articles )
Showing results 1 to 20 of 131.
Sorted by year (- D’Silva, Vijay; Sousa, Marcelo: Complete abstractions and subclassical modal logics (2017)
- Ehlers, Rüdiger; Lafortune, Stéphane; Tripakis, Stavros; Vardi, Moshe Y.: Supervisory control and reactive synthesis: a comparative introduction (2017)
- Jha, Susmit; Seshia, Sanjit A.: A theory of formal synthesis via inductive learning (2017)
- Bouyer, Patricia; Gardy, Patrick; Markey, Nicolas: On the semantics of strategy logic (2016)
- Di Stasio, Antonio; Murano, Aniello; Perelli, Giuseppe; Vardi, Moshe Y.: Solving parity games using an automata-based algorithm (2016)
- Duan, Zhenhua; Tian, Cong; Zhang, Nan: A canonical form based decision procedure and model checking approach for propositional projection temporal logic (2016)
- Shi, Hui-Xian; Li, Yong-Ming: Temporal normal form for linear temporal logic formulae (2016)
- Yang, Fan; Yang, Guowu; Hao, Yujie: The modeling library of eavesdropping methods in quantum cryptography protocols by model checking (2016)
- Zhang, Nan; Duan, Zhenhua; Tian, Cong: A complete axiom system for propositional projection temporal logic with cylinder computation model (2016)
- Zhang, Nan; Duan, Zhenhua; Tian, Cong: A mechanism of function calls in MSVL (2016)
- Ben-David, Shoham; Copty, Fady; Fisman, Dana; Ruah, Sitvanit: Vacuity in practice: temporal antecedent failure (2015)
- Chatterjee, Krishnendu; Henzinger, Thomas A.; Jobstmann, Barbara; Singh, Rohit: Measuring and synthesizing systems in probabilistic environments (2015)
- Laroussinie, François; Markey, Nicolas: Augmenting ATL with strategy contexts (2015)
- von Essen, Christian; Jobstmann, Barbara: Program repair without regret (2015)
- Yatapanage, Nisansala; Winter, Kirsten: Next-preserving branching bisimulation (2015)
- Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Dingzhu: A formal proof of the deadline driven scheduler in PPTL axiomatic system (2014)
- Chockler, Hana; Gurfinkel, Arie; Strichman, Ofer: Beyond vacuity: towards the strongest passing formula (2013)
- Dong, Ruzhen; Faber, Johannes; Ke, Wei; Liu, Zhiming: rCOS: defining meanings of component-based software architectures (2013)
- Duan, Zhenhua; Zhang, Nan; Koutny, Maciej: A complete proof system for propositional projection temporal logic (2013)
- Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)