Book chapter
Formal Analysis of Real-Time Systems with SAM
Formal Methods and Software Engineering, pp 275-286
2002
Abstract
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.
Metrics
Details
- Title
- Formal Analysis of Real-Time Systems with SAM
- Creators
- Huiqun Yu - Florida International UniversityXudong He - Florida International UniversityYi Deng - Florida International UniversityLian Mo - Florida International University
- Publication Details
- Formal Methods and Software Engineering, pp 275-286
- Series
- Lecture Notes in Computer Science
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Resource Type
- Book chapter
- Language
- English
- Academic Unit
- College of Computing and Informatics
- Web of Science ID
- WOS:000181471000030
- Scopus ID
- 2-s2.0-84948974685
- Other Identifier
- 991021868106904721
InCites Highlights
Data related to this publication, from InCites Benchmarking & Analytics tool:
- Collaboration types
- Domestic collaboration
- International collaboration
- Web of Science research areas
- Computer Science, Artificial Intelligence
- Computer Science, Software Engineering