A formal framework for ASTRAL intralevel proof obligations

Author

Coen-Porisini, Alberto ; Kemmerer, Richard A. ; Mandrioli, Dino

Author_Institution

Dipartimento di Elettronica e Inf., Politecnico di Milano, Italy

Volume

20

Issue

8

fYear

1994

fDate

8/1/1994 12:00:00 AM

Firstpage

548

Lastpage

561

Abstract

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL specifications. ASTRAL is provided with structuring mechanisms that allow one to build modularized specifications of complex systems with layering. In this paper, further details of the ASTRAL environment components and the critical requirements components, which were not fully developed in previous papers, are presented. Formal proofs in ASTRAL can be divided into two categories: interlevel proofs and intralevel proofs. The former deal with proving that the specification of level i+1 is consistent with the specification of level i, and the latter deal with proving that the specification of level i is consistent and satisfies the stated critical requirements. This paper concentrates on intralevel proofs

Keywords

finite state machines; formal specification; program verification; real-time systems; specification languages; ASLAN; ASTRAL; TRIO; formal methods; formal proof; formal software development; formal specification; formal specification language; intralevel proof obligations; mathematical correctness; real-time systems; state machines; timing requirements; verification; Automata; Computer science; Formal specifications; Laboratories; Logic functions; Programming; Real time systems; Software; Timing;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.310665

Filename

310665