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.

References in zbMATH (referenced in 111 articles )

Showing results 1 to 20 of 111.
Sorted by year (citations)

1 2 3 4 5 6 next

  1. Bouyer, Patricia; Gardy, Patrick; Markey, Nicolas: On the semantics of strategy logic (2016)
  2. Duan, Zhenhua; Tian, Cong; Zhang, Nan: A canonical form based decision procedure and model checking approach for propositional projection temporal logic (2016)
  3. Zhang, Nan; Duan, Zhenhua; Tian, Cong: A mechanism of function calls in MSVL (2016)
  4. Zhang, Nan; Duan, Zhenhua; Tian, Cong: A complete axiom system for propositional projection temporal logic with cylinder computation model (2016)
  5. Ben-David, Shoham; Copty, Fady; Fisman, Dana; Ruah, Sitvanit: Vacuity in practice: temporal antecedent failure (2015)
  6. Laroussinie, François; Markey, Nicolas: Augmenting ATL with strategy contexts (2015)
  7. von Essen, Christian; Jobstmann, Barbara: Program repair without regret (2015)
  8. Yatapanage, Nisansala; Winter, Kirsten: Next-preserving branching bisimulation (2015)
  9. Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Dingzhu: A formal proof of the deadline driven scheduler in PPTL axiomatic system (2014)
  10. Chockler, Hana; Gurfinkel, Arie; Strichman, Ofer: Beyond vacuity: towards the strongest passing formula (2013)
  11. Duan, Zhenhua; Zhang, Nan; Koutny, Maciej: A complete proof system for propositional projection temporal logic (2013)
  12. Laroussinie, François; Meyer, Antoine; Petonnet, Eudes: Counting $\mathsf CTL$ (2013)
  13. Xia, Mo; Lo, Kueiming; Shao, Shuangjia; Sun, Mian: Formal modeling and verification for MVB (2013)
  14. Beer, Ilan; Ben-David, Shoham; Chockler, Hana; Orni, Avigail; Trefler, Richard: Explaining counterexamples using causality (2012)
  15. Bérard, Béatrice; Haddad, Serge; Sassolas, Mathieu: Interrupt timed automata: verification and expressiveness (2012)
  16. Ndukwu, Ukachukwu: Generating counterexamples for quantitative safety specifications in probabilistic B (2012)
  17. Schuppan, Viktor: Towards a notion of unsatisfiable and unrealizable cores for LTL (2012)
  18. Tian, Cong; Duan, Zhenhua; Zhang, Nan: An efficient approach for abstraction-refinement in model checking (2012)
  19. Basu, Ananda; Bensalem, Saddek; Peled, Doron; Sifakis, Joseph: Priority scheduling of distributed systems based on model checking (2011)
  20. Jörges, Sven; Margaria, Tiziana; Steffen, Bernhard: Assuring property conformance of code generators via model checking (2011)

1 2 3 4 5 6 next