Design of the real time systems using temporal logic specifications: a case study

Abstract

An implementation method for real time systems is proposed in this article. The implementation starts with the design of the functional specifications of the systems behaviour. The functional specifications are introduced as a set of rules describing the partial time ordering of the actions performed by the system. These rules are then written in terms of temporal logic formulae. The temporal logic formulae are checked using Z.Manna-P.Wolper satisfiability analysis procedure [1]. It is known that this procedure generates a state-graph which can be regarded as a state- based automaton of the system. The sate-based automaton is used then to generate the dual (inverted) automaton of the system. The dual automaton is called action-based automaton and can be created using the procedure proposed by authors in [4,5]. Using the action-based automaton of the system the design method introduced in [5,6] is applied to implement the system driver in a systematic manner which can be computerised. The method proposed in this paper is an efficient complementation and generalisation of the results [4,5,6] mentioned above. The method is used for a case study. An elevator control system is designed using the proposed method. The design is carried out in a systematic manner which includes: a) design of functional specifications, b) design of temporal logic specifications, c) satisfiability analysis of temporal logic specifications, d) design of the state-based automaton of the specifications, e) design of the action-based automaton of the system, f) design of the transition activation conditions, g) design of the action activation conditions, h) design of the functional model of the elevator control system, i) implementation of the elevator's actions, j) design of the elevator control system driver.