Practical formal development of real time systems

Steven Bradley; William Henderson; David Kendall; Adrian Robson

doi:10.1109/RTOSS.1994.292563

Practical formal development of real time systems

Steven Bradley, William Henderson, David Kendall, Adrian Robson

Research output: Contribution to conference › Paper › peer-review

2 Citations (Scopus)

Abstract

The complexities of real-time systems are such that it is often thought necessary to give a formal justification of their correctness, especially if they are to be used in a safety-critical environment. In this paper we describe our work on a formally based design method for real-time systems which allows the timing aspects of a concurrent system to be mathematically described and verified, as well as semi-automatically implemented. Our design language, AORTA, is a timed process algebra, with features to ensure that all designs can be implemented. A predictable real-time kernel is also described, which is used in the construction of a system from an AORTA design, and which allows the timing of the implementation to be verified.

Original language	English
DOIs	https://doi.org/10.1109/RTOSS.1994.292563
Publication status	Published - 1994
Event	RTOSS '94: 11th IEEE Workshop on Real-Time Operating Systems and Software - Seattle Duration: 1 Jan 1994 → …

Conference

Conference	RTOSS '94: 11th IEEE Workshop on Real-Time Operating Systems and Software
Period	1/01/94 → …

Access to Document

10.1109/RTOSS.1994.292563

Cite this

@conference{a531859a0fc84f069894db2a8b83b6dd,

title = "Practical formal development of real time systems",

abstract = "The complexities of real-time systems are such that it is often thought necessary to give a formal justification of their correctness, especially if they are to be used in a safety-critical environment. In this paper we describe our work on a formally based design method for real-time systems which allows the timing aspects of a concurrent system to be mathematically described and verified, as well as semi-automatically implemented. Our design language, AORTA, is a timed process algebra, with features to ensure that all designs can be implemented. A predictable real-time kernel is also described, which is used in the construction of a system from an AORTA design, and which allows the timing of the implementation to be verified.",

author = "Steven Bradley and William Henderson and David Kendall and Adrian Robson",

year = "1994",

doi = "10.1109/RTOSS.1994.292563",

language = "English",

note = "RTOSS '94: 11th IEEE Workshop on Real-Time Operating Systems and Software ; Conference date: 01-01-1994",

}

TY - CONF

T1 - Practical formal development of real time systems

AU - Bradley, Steven

AU - Henderson, William

AU - Kendall, David

AU - Robson, Adrian

PY - 1994

Y1 - 1994

N2 - The complexities of real-time systems are such that it is often thought necessary to give a formal justification of their correctness, especially if they are to be used in a safety-critical environment. In this paper we describe our work on a formally based design method for real-time systems which allows the timing aspects of a concurrent system to be mathematically described and verified, as well as semi-automatically implemented. Our design language, AORTA, is a timed process algebra, with features to ensure that all designs can be implemented. A predictable real-time kernel is also described, which is used in the construction of a system from an AORTA design, and which allows the timing of the implementation to be verified.

AB - The complexities of real-time systems are such that it is often thought necessary to give a formal justification of their correctness, especially if they are to be used in a safety-critical environment. In this paper we describe our work on a formally based design method for real-time systems which allows the timing aspects of a concurrent system to be mathematically described and verified, as well as semi-automatically implemented. Our design language, AORTA, is a timed process algebra, with features to ensure that all designs can be implemented. A predictable real-time kernel is also described, which is used in the construction of a system from an AORTA design, and which allows the timing of the implementation to be verified.

U2 - 10.1109/RTOSS.1994.292563

DO - 10.1109/RTOSS.1994.292563

M3 - Paper

T2 - RTOSS '94: 11th IEEE Workshop on Real-Time Operating Systems and Software

Y2 - 1 January 1994

ER -

Practical formal development of real time systems

Abstract

Conference

Access to Document

Fingerprint

Cite this