Safety. liveness and real-time in embedded system design

摘要

Modelling of complex systems should be based on mathematical notions rather than , Modelling of complex systems should be based on mathematical notions rather than being bound tightly to any programming language. Therefore, it is useful to be able being bound tightly to any programming language. Therefore, it is useful to be able to distinguish the different constituents of a distributed and concurrent system. In this paper, we focus on the formal properties known as safety--characterisations of the kind 'nothing bad ever happens' --and liveness--characterisations of the kind 'something good eventually happens'. Since embedded system specitications consist of timing as well l as functional constraints. we also discuss real--time properties and their relation to safety ' and liveness. We represent specifications graphically using the Temporal Logic of Actions, a logic that models system behaviour by sequences of states. The main part of this paper is a case study where we model an access cycle in the Industry Standard Architecture (ISA) bus. based on an abstract channel specification.