Bookbot

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

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

Pubblicazione

Acquisto del libro

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

Lingua
Pubblicato
2004
product-detail.submit-box.info.binding
(In brossura)
Ti avviseremo via email non appena lo rintracceremo.

Metodi di pagamento