News

Overview

Real-time systems are systems that must perform a task within strict time deadlines. Embedded controllers, circuits and communication protocols are examples of such time- dependent systems. These systems are often part of complex safety-critical applications such as aircraft avionics, which are very difficult to design and analyze, but whose correct behavior must beensured because failures may have severe consequences. Hence, real- time systems need to be rigorously modeled and specified in order to be able to formally prove their correctness with respect to the desired requirements.

The systems are described in RAVEN as interacting modules. Each module is an I/O-interval structure. I/O-interval structures extends finite state machines (FSM) by timed transitions. The modules are connected by wires (resp. communicate via broadcast).

RAVEN has several algorithms for analyzing the specified system:

• Dead- and live-lock tests may be performed to check wether the system may reach states in which no time progress is possible (dead-lock) or states which may never be left (live-lock).
• Model checking allows the user to specify properties in the temporal logic CCTL (clocked computation tree logic), which may be verified automatically by RAVEN. If the given system do not hold the specification, a counter example may be generated wich shows an execution sequence making the failure clear.
• Min/max computation allows to quantitative analyse the the system. There exist three algorithms: stable computes the maximal number of time steps a formula hold; min computes the minimal path from a set of start sets to a set of destination states; max computes the maximal path from a set of start sets to a set of destination states.

RAVEN allows to simulate the system. The result is a waveform displayed in a waveform browser.