Formal Analysis of Real-Time Systems

View Sample PDF

Author(s): Osman Hasan (National University of Science and Technology (NUST), Pakistan)and Sofiène Tahar (Concordia University, Canada)
Copyright: 2011
Pages: 34
Source title: Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility
Source Author(s)/Editor(s): Mohamed Khalgui (Xidian University, China)and Hans-Michael Hanisch (Martin Luther University, Germany)
DOI: 10.4018/978-1-60960-086-0.ch013

Keywords: Computer Science & IT / Information Science Reference / Systems & Software Design / Systems and Software Engineering

Purchase

View Formal Analysis of Real-Time Systems on the publisher's website for pricing and purchasing information.

Abstract

Real-time systems usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism, which makes their performance analysis quite complex. Thus, traditional techniques, such as simulation, or state-based formal methods usually fail to produce reasonable results. The main limitation of these approaches may be overcome by conducting the performance analysis of real-time systems using higher-order-logic theorem proving. This chapter is mainly oriented towards this emerging trend and it provides the details about analyzing both functional and performance related properties of real-time systems using a higher-order-logic theorem prover (HOL). For illustration purposes, the Stop-and-Wait protocol, which is a classical example of real-time systems, has been considered as a case-study.

The IRMA Community

Research IRM

Formal Analysis of Real-Time Systems

Purchase

Abstract

Related Content

IRMA Sponsors