XTG-an engineering approach to modelling and analysis of real-time systems
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The paper addresses the ongoing research on verification and simulation of real time systems at SEPC. The approach taken is an engineering approach dedicated to tool development aiming at a wider dissemination of formal methods and techniques in industrial application. The tool environment under construction TVS, is dedicated to formal verification and simulation of real time systems. TVS comprises language front ends for both specification and implementation languages, a verification notation XTG and a simulation language SL. XTG is a new formalism for describing real time systems. It is an engineering notation based on timed automata aimed at providing a simple representation for high level specification languages. By translating a high level specification into an XTG system, a representation is obtained that better suits the application of automatic verification and simulation techniques. XTG is suited as concrete representation for languages that allow extensive modeling of data, have a maximal progress semantics, and model interprocess communication by value passing through data channels.Keywords
This publication has 8 references indexed in Scilit:
- Ada 95 as implementation vehicle for formal specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Automatic analysis of embedded systems specified in AstralPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Experiences with analysis of formal specifications in AstralPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Timing analysis of Ada tasking programsIEEE Transactions on Software Engineering, 1996
- A Compositional Proof of a Real-Time Mutual Exclusion ProtocolBRICS Report Series, 1996
- The algorithmic analysis of hybrid systemsTheoretical Computer Science, 1995
- Model-checking for real-time systemsPublished by Springer Nature ,1995
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986