Specification, modelling, verification and runtime analysis of real time systems

Autori

• Georgios Logothetis

Parametri

• Computer, IT, programmazione
• Dissertationen zur künstlichen Intelligenz

Maggiori informazioni sul libro

This book explores the application of formal methods to ensure the correctness of real-time systems. It introduces the formal framework Equinox, which facilitates the specification, modeling, verification, and runtime analysis of these systems. Advanced methods enable a formally verifiable design and development process directly from synchronous languages, bridging the gap between industrial real-time descriptions and formal verification. Previous approaches required specific real-time description formats, but this work introduces timed Kripke structures as formal models that allow for abstractions in real-time systems without compromising quantitative properties. The framework supports modeling non-interruptible processes and atomic timed actions, which is crucial for low-level verification. Additionally, a new temporal logic, JCTL, is developed as a real-time extension of the widely used CTL, addressing issues found in other real-time logics. JCTL is defined on timed Kripke structures, allowing the application of established symbolic techniques. The book also presents sophisticated methods for efficiently handling parallel process execution, enabling the direct generation of a formal model without the need for parallel composition of sub-models, thus mitigating problems like state space explosion, deadlocks, and timelocks. Finally, a detailed low-level runtime analysis is introduced, combining the modeling capabilities of ti

Per saperne di più

Lingua: Inglese

Pubblicato: 2004

(In brossura)