Formally Specifying and Verifying Real-Time Systems

A real-time computer system is a system that must perform its functions within specified time bounds. These systems are generally characterized by complex interactions with the environment in which they operate and strict time constraints whose violation may have catastrophic consequences. The need for these software systems to be highly reliable is evident. One way to achieve this reliability is through formal development. Although research in the area of real-time systems has been quite active and a number of experimental environments supporting formal specifications have been developed, the search for adequate notations and tools is still ongoing. In order to get designers to use formal methods to develop real-time systems it is necessary to provide them with an integrated set of tools for writing and analyzing their specifications. The ASTRAL Software Development Environment (SDE), which is an integrated set of tools based on the ASTRAL formal framework, is intended to meet this n...

• Type: Conference
• Year: 1997
• Where: ICFEM
• Authors: Richard A. Kemmerer
• Keywords: ASTRAL Software Development, ICFEM 1997, Real-time Systems, Software Development Environment, Software Engineering