Modeling and Checking Real-Time System Designs

Resumen

Real-time systems are found in an increasing variety of application elds. Usually, they are embedded systems controlling devices that may risk lives or damage properties: they are safety critical systems. Hard Real-Time requirements (late means wrong) make the development of such kind of systems a formidable and daunting task.
The need to predict temporal behavior of critical real-time systems has encouraged the development of an useful collection of models, results and tools for analyzing schedulability of applications. However, there is no general analytical support for verifying other kind of high level timing requirements on complex software architectures. On the other hand, the verication of specications and designs of real-time systems has been considered an interesting application eld for automatic analysis techniques such as model-checking. Unfortunately, there is a natural trade-o between sophistication of supported features and the practicality of formal analysis.