caesar - compilation & verification of LOTOS specifications. caesar [Gar89b,GS90] is a compiler that translates a LOTOS specification into executable code that can be used to explore, on-the-fly or exhaustively, the graph (also called labelled transition system, reachability graph, state space, etc.) corresponding to the behaviour of this specification. caesar itself does not embody verification capabilities, but it smootly interfaces with many tools that can perform explicit-state and on-the-fly verification on the generated graph, including model checking, equivalence checking, and visual checking. Taking as input filename.lotos, which contains a LOTOS specification, optionally accompanied by filename.h, which provides C types and functions implementing the LOTOS sorts and operations defined in filename.lotos, caesar performs successive transformation steps and produces a C program that allows to execute, simulate, and/or build the corresponding graph. In the latter case, the result of caesar is the graph itself, rather than the C program, which is removed after its execution.
Keywords for this software
References in zbMATH (referenced in 8 articles , 2 standard articles )
Showing results 1 to 8 of 8.
- Garavel, Hubert: Nested-unit Petri nets (2019)
- Gallardo, M. M.; Joubert, C.; Merino, P.; Sanán, D.: A model-extraction approach to verifying concurrent C programs with CADP (2012) ioport
- Garavel, Hubert; Lang, Frédéric; Mateescu, Radu; Serwe, Wendelin: CADP 2010: a toolbox for the construction and analysis of distributed processes (2011)
- Lang, Frédéric; Salaün, Gwen; Hérilier, Rémi; Kramer, Jeff; Magee, Jeff: Translating FSP into LOTOS and networks of automata (2010)
- Garavel, Hubert; Salaün, Gwen; Serwe, Wendelin: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP (2009)
- Garavel, Hubert: Reflections on the future of concurrency theory in general and process calculi in particular (2008)
- Garavel, Hubert; Serwe, Wendelin: State space reduction for process algebra specifications (2006)
- Garavel, Hubert; Serwe, Wendelin: State space reduction for process algebra specifications (2004)