Abstract
This work presents an integrated approach which covers from the formal specification to the analysis and use of tools to prove properties about real-time systems. The proposed language to specify the system behaviour is Timed-CSP-Z, a combination of Timed CSP and Z. We propose a rule-based strategy for converting a Timed-CSP-Z specification to TER Nets, a high level Petri Net based formalism with time. The conversion enables us to use the CABERNET tool to analyse desired properties. As a practical case study we discuss the application of this approach to the specification and analysis of an On-board Computer of a Brazilian microsatellite. © Springer-Verlag Berlin Heidelberg 2001.
Cite
CITATION STYLE
Sherif, A., Sampaio, A., & Cavalcante, S. (2001). An integrated approach to specification and validation of real-time systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2021 LNCS, pp. 278–299). Springer Verlag. https://doi.org/10.1007/3-540-45251-6_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
