DSpace Repository

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

Show simple item record

dc.contributor.author URSU, A.
dc.contributor.author DUBENETSKY, V.
dc.contributor.author GRUITA, G.
dc.date.accessioned 2020-12-18T10:18:44Z
dc.date.available 2020-12-18T10:18:44Z
dc.date.issued 1996
dc.identifier.citation URSU, A., DUBENETSKY, V., GRUITA, G. Design of the real time systems using temporal logic specifications: a case study. In: Computer Science Journal of Moldova. 1996, Vol 4, nr. 1 (10), pp.88-114. ISSN 1561-4042. en_US
dc.identifier.uri http://repository.utm.md/handle/5014/12196
dc.description.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. en_US
dc.language.iso en en_US
dc.publisher Institute of Mathematics and Computer Science en_US
dc.rights Attribution-NonCommercial-NoDerivs 3.0 United States *
dc.rights.uri http://creativecommons.org/licenses/by-nc-nd/3.0/us/ *
dc.subject real time systems en_US
dc.subject elevator control system en_US
dc.title Design of the real time systems using temporal logic specifications: a case study en_US
dc.type Article en_US


Files in this item

The following license files are associated with this item:

This item appears in the following Collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivs 3.0 United States Except where otherwise noted, this item's license is described as Attribution-NonCommercial-NoDerivs 3.0 United States

Search DSpace


Advanced Search

Browse

My Account