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

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

1 2 3 ... 7 8 9 next

  1. Bérard, B.; Haddad, S.; Picaronny, C.; Safey El Din, M.; Sassolas, M.: Polynomial interrupt timed automata: verification and expressiveness (2021)
  2. Cousot, Patrick: Calculational design of a regular model checker by abstract interpretation (2021)
  3. Hossain, Akash; Laroussinie, François: (\mathsfQCTL) model-checking with (\mathsfQBF) solvers (2021)
  4. Beneš, Nikola; Fahrenberg, Uli; Křetínský, Jan; Legay, Axel; Traonouez, Louis-Marie: Logical vs. behavioural specifications (2020)
  5. Gardy, Patrick; Bouyer, Patricia; Markey, Nicolas: Dependences in strategy logic (2020)
  6. Saddem-yagoubi, Rim; Naud, Olivier; Godary-dejean, Karen; Crestani, Didier: Model-checking precision agriculture logistics: the case of the differential harvest (2020)
  7. Tellez, Gadi; Brotherston, James: Automatically verifying temporal properties of pointer programs with cyclic proof (2020)
  8. Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei: A novel approach to verifying context free properties of programs (2020)
  9. Zhao, Liang; Wang, Xiaobing; Shu, Xinfeng; Zhang, Nan: A sound and complete proof system for a unified temporal logic (2020)
  10. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  11. 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)
  12. Ho, Hsi-Ming; Ouaknine, Joël; Worrell, James: On the expressiveness and monitoring of metric temporal logic (2019)
  13. Jensen, L. S.; Kaufmann, I.; Larsen, K. G.; Nielsen, S. M.; Srba, J.: Model checking and synthesis for branching multi-weighted logics (2019)
  14. Kupferman, Orna; Vardi, Gal: Flow logic (2019)
  15. Zhao, Liang; Wang, Xiaobing; Duan, Zhenhua: Model checking of pushdown systems for projection temporal logic (2019)
  16. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut: Introduction to model checking (2018)
  17. Gardy, Patrick; Bouyer, Patricia; Markey, Nicolas: Dependences in strategy logic (2018)
  18. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  19. Gregorio-Rodríguez, Carlos; Llana, Luis; Martínez, Rafael: An axiomatic semantics for (\mathsfioco\underline\mathsfs) conformance relation (2018)
  20. Kurshan, Robert P.: Transfer of model checking to industrial practice (2018)

1 2 3 ... 7 8 9 next