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 156 articles )

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

1 2 3 ... 6 7 8 next

  1. Beneš, Nikola; Fahrenberg, Uli; Křetínský, Jan; Legay, Axel; Traonouez, Louis-Marie: Logical vs. behavioural specifications (2020)
  2. Gardy, Patrick; Bouyer, Patricia; Markey, Nicolas: Dependences in strategy logic (2020)
  3. Tellez, Gadi; Brotherston, James: Automatically verifying temporal properties of pointer programs with cyclic proof (2020)
  4. Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei: A novel approach to verifying context free properties of programs (2020)
  5. Zhao, Liang; Wang, Xiaobing; Shu, Xinfeng; Zhang, Nan: A sound and complete proof system for a unified temporal logic (2020)
  6. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  7. Bloem, Roderick; Fey, Goerschwin; Greif, Fabian; Könighofer, Robert; Pill, Ingo; Riener, Heinz; Röck, Franz: Synthesizing adaptive test strategies from temporal logic specifications (2019)
  8. Ho, Hsi-Ming; Ouaknine, Joël; Worrell, James: On the expressiveness and monitoring of metric temporal logic (2019)
  9. Jensen, L. S.; Kaufmann, I.; Larsen, K. G.; Nielsen, S. M.; Srba, J.: Model checking and synthesis for branching multi-weighted logics (2019)
  10. Kupferman, Orna; Vardi, Gal: Flow logic (2019)
  11. Zhao, Liang; Wang, Xiaobing; Duan, Zhenhua: Model checking of pushdown systems for projection temporal logic (2019)
  12. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut: Introduction to model checking (2018)
  13. Gardy, Patrick; Bouyer, Patricia; Markey, Nicolas: Dependences in strategy logic (2018)
  14. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  15. Gregorio-Rodríguez, Carlos; Llana, Luis; Martínez, Rafael: An axiomatic semantics for (\mathsfioco\underline\mathsfs) conformance relation (2018)
  16. Kurshan, Robert P.: Transfer of model checking to industrial practice (2018)
  17. Piterman, Nir; Pnueli, Amir: Temporal logic and fair discrete systems (2018)
  18. Shankar, Natarajan: Combining model checking and deduction (2018)
  19. D’Silva, Vijay; Sousa, Marcelo: Complete abstractions and subclassical modal logics (2017)
  20. Ehlers, Rüdiger; Lafortune, Stéphane; Tripakis, Stavros; Vardi, Moshe Y.: Supervisory control and reactive synthesis: a comparative introduction (2017)

1 2 3 ... 6 7 8 next