×

Formal analysis of real-time systems with SAM. (English) Zbl 1015.68669

George, Chris (ed.) et al., Formal methods and software engineering. 4th international conference on formal engineering methods, ICFEM 2002, Shanghai, China, October 21-25, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2495, 275-286 (2002).
Summary: The Software Architecture Model (SAM) is a general software architecture model based on a dual formalism combining Petri nets and temporal logic. This paper proposes a formal method for modeling and analyzing real-time systems with SAM. A high level Petri net and a linear time temporal logic are used as the theoretical basis for SAM. Behaviors of real-time systems are modeled by Petri nets, while their properties are specified by temporal logic. By translating Petri nets into clocked transition systems, we can apply the Stanford Temporal Prover to automating the analysis of real-time systems. A case study of interactive multimedia documents demonstrates our approach to modeling and analyzing real-time systems with SAM.
For the entire collection see [Zbl 1012.68851].

MSC:

68U99 Computing methodologies and applications
68N99 Theory of software
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

STeP
PDFBibTeX XMLCite
Full Text: Link