Experiences with analysis of formal specifications in Astral
- 23 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
An important issue in the design and implementation of real-time software is the verification of (temporal) properties. Our research of the past few years focused on requirements specification of real-time software and the use of tools in modeling and design. The development of a correct and complete requirements specification is difficult, and therefore tool support is considered important. Our development approach, builds upon requirements specifications constructed using the formal real-time specification language Astral. The development framework offers support for end-users in the construction of a software requirements specifications in Astral. Such end-risers are, for example, control engineers in the area of embedded, real-time control software. Support in the construction of an Astral specification through the use of analysis tools is important because it provides the user with (i) evidence concerning the correctness of the specification and (ii) feasibility of its implementation. This paper describes our development framework focusing on four approaches that have been employed in (timing) analysis of Astral specifications. The first two approaches, simulation and prototyping, are informal, while the latter two are formal, based on a translation into an extension of timed automata.Keywords
This publication has 15 references indexed in Scilit:
- Closed world specification of embedded real-time controllersPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Ada 95 as implementation vehicle for formal specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Issues in real-time process controller realizationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Timing analysis of Ada tasking programsIEEE Transactions on Software Engineering, 1996
- Evaluating deadlock detection methods for concurrent softwareIEEE Transactions on Software Engineering, 1996
- Verification of an Audio Protocol with bus collision using UppaalPublished by Springer Nature ,1996
- Verifying ET-LOTOS programs with KRONOSPublished by Springer Nature ,1995
- A formal framework for ASTRAL intralevel proof obligationsIEEE Transactions on Software Engineering, 1994
- From ATP to timed graphs and hybrid systemsActa Informatica, 1993
- The theory of timed automataPublished by Springer Nature ,1992