{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:49:16Z","timestamp":1761806956369},"reference-count":145,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1992,4,1]],"date-time":"1992-04-01T00:00:00Z","timestamp":702086400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Systems and Software"],"published-print":{"date-parts":[[1992,4]]},"DOI":"10.1016\/0164-1212(92)90045-l","type":"journal-article","created":{"date-parts":[[2003,8,7]],"date-time":"2003-08-07T23:44:36Z","timestamp":1060299876000},"page":"33-60","source":"Crossref","is-referenced-by-count":73,"title":["Formal methods for the specification and design of real-time safety critical systems"],"prefix":"10.1016","volume":"18","author":[{"given":"Jonathan S.","family":"Ostroff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0164-1212(92)90045-L_bib1","doi-asserted-by":"crossref","DOI":"10.1145\/1005928.1005929","article-title":"The bug heard round the world","author":"Garman","year":"1981","journal-title":"ACM SIGSOFT Software Eng. Not."},{"key":"10.1016\/0164-1212(92)90045-L_bib2","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.108047","article-title":"Biting the silver bullet: towards a brighter future for system development","volume":"25","author":"Harel","year":"1992","journal-title":"Computer"},{"key":"10.1016\/0164-1212(92)90045-L_bib3","doi-asserted-by":"crossref","DOI":"10.1145\/359763.359798","article-title":"Towards a discipline of real-time programming","volume":"20","author":"Wirth","year":"1977","journal-title":"Commun. ACM"},{"key":"10.1016\/0164-1212(92)90045-L_bib4","series-title":"Logics and Models of Concurrent Systems","first-page":"477","article-title":"On the development of reactive systems","author":"Harel","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib5","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/MCS.1985.1104956","article-title":"Research needs in manufacturing systems","volume":"5","author":"Cassidy","year":"1985","journal-title":"IEEE Control Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib6","series-title":"Verification and Validation of Real-Time Software","author":"Quirk","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib7","article-title":"Challenges to control: a collective view","volume":"AC-32","author":"Levis","year":"1987","journal-title":"IEEE Trans. Auto. Control"},{"key":"10.1016\/0164-1212(92)90045-L_bib8","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/2.7053","article-title":"Misconceptions about real-time computing: a serious problem for next generation systems","volume":"21","author":"Stankovic","year":"1988","journal-title":"Computer"},{"key":"10.1016\/0164-1212(92)90045-L_bib9","series-title":"Real Time System Design","author":"Levi","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib10","series-title":"Technical Report TR 88-220","article-title":"Evaluation Standards for Safety-Critical Software","author":"Parnas","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib11","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/BF01941129","article-title":"Time considered irrelevant for real-time systems","volume":"28","author":"Turski","year":"1988","journal-title":"BIT"},{"key":"10.1016\/0164-1212(92)90045-L_bib12","article-title":"Foundations of computer science: leaving the ivory tower","author":"de Roever","year":"1991","journal-title":"EATCS Bull."},{"key":"10.1016\/0164-1212(92)90045-L_bib13","series-title":"Foundations of Real-Time Computing: Formal Specifications and Methods","article-title":"Towards mechanization of real-time system design","author":"Mok","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib14","series-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"key":"10.1016\/0164-1212(92)90045-L_bib15","series-title":"Technical Report RR129","article-title":"Formal Description of Real-Time Systems: A Review","author":"Joseph","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib16","series-title":"Technical Report","article-title":"The Formal Development of Real-Time Systems","author":"Scholefield","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib17","series-title":"Reference Manual for the Ada Programming Language","author":"USDOD","year":"1983"},{"key":"10.1016\/0164-1212(92)90045-L_bib18","series-title":"CCIT High Level Language CHILL Recommendation z.200","author":"CCIT","year":"1980"},{"key":"10.1016\/0164-1212(92)90045-L_bib19","series-title":"Occam Programming manual","article-title":"International Series in Computer Science","author":"INMOS Limited","year":"1984"},{"key":"10.1016\/0164-1212(92)90045-L_bib20","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1109\/TSE.1985.232231","article-title":"Dynamic configuration for distributed systems","volume":"SE-11","author":"Kramer","year":"1985","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib21","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1109\/32.24720","article-title":"Constructing distributed systems in Conic","volume":"15","author":"Magee","year":"1989","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib22","series-title":"Strategies for Real-Time System Specification","author":"Hatley","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib23","series-title":"Structural Development for Real-Time Systems","author":"Ward","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib24","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts: a visual formalism for complex systems","volume":"8","author":"Harel","year":"1987","journal-title":"Sci. Comp. Progr."},{"key":"10.1016\/0164-1212(92)90045-L_bib25","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1109\/32.54292","article-title":"Statemate: a working environment for the development of complex reactive systems","volume":"16","author":"Harel","year":"1990","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib26","series-title":"Proceedings of the 9th Real-Time Systems Symposium","first-page":"2","article-title":"State-based specification of complex real-time systems","author":"Gabrielian","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib27","series-title":"Technical Report","article-title":"Analysis Capabilities for Requirements Specified in Statecharts","author":"Melhart","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib28","series-title":"Ph.D. Thesis","article-title":"Semantics of Reactive Systems: Comparison and Full Abstraction","author":"Huizing","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib29","series-title":"Theoretical Aspects of Computer Software","first-page":"244","article-title":"What is in a step?","author":"Pnueli","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib30","series-title":"Technical Report","article-title":"The Esterel Synchronous Programming Language: Design, Semantics, Implementation","author":"Berry","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib31","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1109\/9.53519","article-title":"Hybrid dynamical systems theory and the SIGNAL language","volume":"35","author":"Benveniste","year":"1990","journal-title":"IEEE Trans. Auto. Control"},{"key":"10.1016\/0164-1212(92)90045-L_bib32","series-title":"Proceedings of the 14th ACM Symposium on Programming Languages","article-title":"LUSTRE: a declarative language for programming synchronous systems","author":"Caspi","year":"1987"},{"key":"10.1016\/0164-1212(92)90045-L_bib33","series-title":"Petri Net Theory and the Modelling of Systems","author":"Peterson","year":"1981"},{"key":"10.1016\/0164-1212(92)90045-L_bib34","series-title":"Petri Nets: An Introduction","author":"Reisig","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib35","series-title":"Proceedings of the International Conference on Fifth Generation Computer Systems","article-title":"Some directions in concurrency theory (panel statement)","author":"Milner","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib36","series-title":"Proceedings of Logics of Programs","first-page":"167","article-title":"Compositional semantics for real-time distributed computing","author":"Koymans","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib37","doi-asserted-by":"crossref","first-page":"1080","DOI":"10.1109\/TSE.1987.232850","article-title":"Interactive state-space analysis of concurrent systems","volume":"SE-13","author":"Morgan","year":"1987","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib38","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1109\/32.4651","article-title":"PROTEAN: a high-level Petri net tool for the specification and verification of communication protocols","volume":"14","author":"Billington","year":"1988","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib39","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","article-title":"Recoverability of communication protocols\u2014implications of a theoretical study","author":"Merlin","year":"1976","journal-title":"IEEE Trans. Commun."},{"key":"10.1016\/0164-1212(92)90045-L_bib40","series-title":"Technical Report MAC TR 120","article-title":"Analysis of Asynchronous Concurrent Systems by Timed Petri Nets","author":"Ramchandani","year":"1974"},{"key":"10.1016\/0164-1212(92)90045-L_bib41","series-title":"Proceedings of the 7th Annual Symposium on Computer Architecture","article-title":"Timed Petri nets and preliminary performance evaluation","author":"Zubrek","year":"1980"},{"key":"10.1016\/0164-1212(92)90045-L_bib42","series-title":"Proceedings of the 4th International Workshop on Protocol Verification and Testing","article-title":"Performance analysis of timed Petri nets","author":"Razouk","year":"1984"},{"key":"10.1016\/0164-1212(92)90045-L_bib43","series-title":"International Workshop on Timed Petri Nets, IEEE Computer Society","first-page":"162","article-title":"PAREDE: an automated tool for the analysis of time(d) Petri nets","author":"Menasche","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib44","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1109\/TSE.1987.233170","article-title":"Safety analysis using Petri nets","volume":"SE-13","author":"Leveson","year":"1987","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib45","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","article-title":"Modeling and verification of time dependent systems using time petri nets","volume":"17","author":"Berthomieu","year":"1991","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib46","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1109\/32.75416","article-title":"Rule based design methodology for solving control problems","volume":"17","author":"Etessami","year":"1991","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib47","series-title":"Ph.D. Thesis","article-title":"Timed Coloured Petri Nets and their Applications to Logistics","author":"van der Aalst","year":"1992"},{"key":"10.1016\/0164-1212(92)90045-L_bib48","series-title":"Proceedings of the 28th IEEE Conference on Decision and Control","article-title":"Synthesis of controllers for real-time discrete event systems","author":"Ostroff","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib49","series-title":"Proceedings of the ECC91 European Control Conference, Hermes Press","first-page":"522","article-title":"Systematic development of real-time discrete event systems","author":"Ostroff","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib50","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/32.75414","article-title":"Software requirements analysis for real time process control systems","volume":"17","author":"Jaffe","year":"1991","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib51","series-title":"CRL Report 237","article-title":"Functional Documentation for Computer Systems Engineering","author":"Parnas","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib52","series-title":"Proceedings of the REX Workshop \u201cReal-Time: Theory in Practice\u201d","article-title":"Forward and backward simulations for timing-based systems","author":"Lynch","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib53","series-title":"Systematic Software Development using VDM","author":"Jones","year":"1986"},{"key":"10.1016\/0164-1212(92)90045-L_bib54","series-title":"The Z Notation: A Reference Manual","author":"Spivey","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib55","series-title":"Temporal Logic in specification","article-title":"Using temporal logic for prototyping: the design of a lift controller","author":"Hale","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib56","doi-asserted-by":"crossref","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/0164-1212(92)90045-L_bib57","series-title":"The Science of Programming","author":"Gries","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib58","doi-asserted-by":"crossref","DOI":"10.1145\/360051.360224","article-title":"Verifying properties of parallel programs: an axiomatic approach","volume":"19","author":"Owicki","year":"1976","journal-title":"Commun. ACM"},{"key":"10.1016\/0164-1212(92)90045-L_bib59","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","article-title":"Supervisory control of a class of discrete-event processes","volume":"25","author":"Ramadge","year":"1987","journal-title":"SIAM J. Control Optim."},{"key":"10.1016\/0164-1212(92)90045-L_bib60","doi-asserted-by":"crossref","first-page":"1202","DOI":"10.1137\/0325066","article-title":"Modular feedback logic for discrete event systems","volume":"25","author":"Ramadge","year":"1987","journal-title":"SIAM J. Control Optim."},{"key":"10.1016\/0164-1212(92)90045-L_bib61","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1109\/9.1271","article-title":"Finitely recursive process models for discrete event systems","volume":"33","author":"Inan","year":"1988","journal-title":"IEEE Trans. Auto. Control"},{"key":"10.1016\/0164-1212(92)90045-L_bib62","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1109\/9.381","article-title":"Principles and engineering of process control with Petri nets","volume":"33","author":"Brand","year":"1988","journal-title":"IEEE Trans. Auto. Control"},{"key":"10.1016\/0164-1212(92)90045-L_bib63","series-title":"Systems Control Group Report No 9106","article-title":"Control of Vector Discrete-Event Systems","author":"Li","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib64","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","article-title":"Synthesis of communicating processes from temporal logic specifications","volume":"6","author":"Manna","year":"1984","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib65","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","article-title":"Using branching time temporal logic to synthesize synchronization skeletons","volume":"2","author":"Emerson","year":"1982","journal-title":"Sci. Comp. Progr."},{"key":"10.1016\/0164-1212(92)90045-L_bib66","series-title":"Proceedings of the 14th ACM Symposium of Principles of Programming Languages","first-page":"1","article-title":"Specification and verification of concurrent program\u2200-automata","author":"Manna","year":"1987"},{"key":"10.1016\/0164-1212(92)90045-L_bib67","doi-asserted-by":"crossref","DOI":"10.1145\/59287.62028","article-title":"Verifying temporal properties without temporal logic","volume":"11","author":"Alpern","year":"1989","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib68","series-title":"Parallel Program Design","author":"Chandy","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib69","series-title":"Temporal Logic for Real-Time Systems","author":"Ostroff","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib70","series-title":"Temporal Logic","author":"Rescher","year":"1971"},{"key":"10.1016\/0164-1212(92)90045-L_bib71","series-title":"Temporal Logics and their Applications","year":"1987"},{"key":"10.1016\/0164-1212(92)90045-L_bib72","series-title":"Proceedings of the 18th IEEE Annual Symposium on the Foundations of Computer Science","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/0164-1212(92)90045-L_bib73","series-title":"Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages","first-page":"174","article-title":"\u2018Sometime\u2019 is sometimes \u2018not never,\u2019","author":"Lamport","year":"1980"},{"key":"10.1016\/0164-1212(92)90045-L_bib74","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","article-title":"Proving liveness properties of concurrent programs","volume":"4","author":"Owicki","year":"1982","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib75","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","article-title":"Specifying concurrent program modules","volume":"5","author":"Lamport","year":"1983","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib76","series-title":"Information Processing 83","first-page":"657","article-title":"What good is temporal logic?","author":"Lamport","year":"1983"},{"key":"10.1016\/0164-1212(92)90045-L_bib77","series-title":"Fairness","author":"Francez","year":"1986"},{"key":"10.1016\/0164-1212(92)90045-L_bib78","article-title":"Temporal Logics of Programs","volume":"vol. 8","author":"Kroger","year":"1987"},{"key":"10.1016\/0164-1212(92)90045-L_bib79","article-title":"From state machines to temporal logic: specification methods for protocol standards","volume":"Com-30","author":"Schwartz","year":"1982","journal-title":"IEEE Trans. Commun."},{"key":"10.1016\/0164-1212(92)90045-L_bib80","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","article-title":"A temporal logic for multilevel reasoning about hardware","volume":"18","author":"Moszkowski","year":"1985","journal-title":"Computer"},{"key":"10.1016\/0164-1212(92)90045-L_bib81","series-title":"Proceedings Real-Time Systems Symposium, IEEE Computer Society","first-page":"86","article-title":"Specification of real-time systems in real-time temporal interval logic","author":"Narayana","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib82","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"(Real) time: a philosphical perspective","author":"Koymans","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib83","series-title":"Technical Report","article-title":"Verification of Concurrent Programs: A Temporal Proof System","author":"Manna","year":"1983"},{"key":"10.1016\/0164-1212(92)90045-L_bib84","series-title":"Current Trends in concurrency","article-title":"Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends","author":"Pnueli","year":"1986"},{"key":"10.1016\/0164-1212(92)90045-L_bib85","series-title":"Models of Concurrency: Linear, Branching and Partial Orders","article-title":"The anchored version of the temporal framework","author":"Manna","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib86","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"\u201cSometimes\u2019 and \u2018not never\u2019 revisited: on branching versus linear time temporal logic","volume":"33","author":"Emerson","year":"1986","journal-title":"J. Assoc. Comp. Mach."},{"key":"10.1016\/0164-1212(92)90045-L_bib87","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite state concurrent systems using temporal logic","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib88","series-title":"Proceedings of PARLE 89","article-title":"A temporal logic based compositional proof system for real-time message passing","volume":"vol. II","author":"Hooman","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib89","series-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","year":"1992"},{"key":"10.1016\/0164-1212(92)90045-L_bib90","series-title":"Proceedings of ACM SIGOPS 8th annual ACM Symposium on Operating Systems Principles","first-page":"1","article-title":"Proving real-time properties of programs with temporal logic","author":"Bernstein","year":"1981"},{"key":"10.1016\/0164-1212(92)90045-L_bib91","series-title":"Proceedings of the 2nd Annual Symposium on Principles of Distributed Computing","first-page":"187","article-title":"Real time programming and asynchronous message passing","author":"Koymans","year":"1983"},{"key":"10.1016\/0164-1212(92)90045-L_bib92","series-title":"Proceedings of the 24th IEEE Conference on Decision and Control","first-page":"656","article-title":"A temporal logic approach to real time control","author":"Ostroff","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib93","series-title":"Technical Report 8618","article-title":"Real-Time Computer Control of Discrete Event Systems Modelled by Extended State Machines: A Temporal Logic Approach","author":"Ostroff","year":"1986"},{"key":"10.1016\/0164-1212(92)90045-L_bib94","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/71.80145","article-title":"Deciding properties of timed transition models","volume":"1","author":"Ostroff","year":"1990","journal-title":"IEEE Trans. Parallel Dist. Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib95","doi-asserted-by":"crossref","DOI":"10.1109\/9.52290","article-title":"A framework for real-time discrete event control","author":"Ostroff","year":"1990","journal-title":"IEEE Trans. Auto. Control"},{"key":"10.1016\/0164-1212(92)90045-L_bib96","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF00365462","article-title":"A verifier for real-time properties","volume":"4","author":"Ostroff","year":"1992","journal-title":"Real Time J."},{"key":"10.1016\/0164-1212(92)90045-L_bib97","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"Verification of safety critical systems using TTM\/RTTI","author":"Ostroff","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib98_1","series-title":"Master's Thesis","article-title":"Transformational Equivalence of Timed Transition Models","author":"Lawford","year":"1992"},{"key":"10.1016\/0164-1212(92)90045-L_bib98_2","author":"Lawford","year":"1992","journal-title":"Systems Control Group Report No. 9202"},{"issue":"number 3C4","key":"10.1016\/0164-1212(92)90045-L_bib99","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0743-1066(91)90028-N","article-title":"Constraint logic programming for reasoning about discrete event processes","volume":"Volume II","author":"Ostroff","year":"1991","journal-title":"J. Log. Progr."},{"key":"10.1016\/0164-1212(92)90045-L_bib100","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying real-time properties with metric temporal logic","volume":"2","author":"Koymans","year":"1990","journal-title":"Real-Time Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib101","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","article-title":"Safety analysis of timing properties in real-time systems","volume":"SE-12","author":"Jahanian","year":"1986","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib102","series-title":"Ph.D. Thesis","article-title":"The Temporal Specification and Verification of Real-Time Systems","author":"Henzinger","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib103","series-title":"Formal Techniques in Real-Time and Fault Tolerant Systems","article-title":"Applications of temporal logic to the specification of real-time systems","author":"Pnueli","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib104","series-title":"Proceedings of the 18th ACM Symposium on Principles of Programming Languages","first-page":"353","article-title":"Temporal proof methodologies for real-time systems","author":"Henzinger","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib105","series-title":"Ph.D. Thesis","article-title":"Specification and Compositional Verification of Real-Time Systems","author":"Hooman","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib106","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"Logics and models of real-time: a survey","author":"Alur","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib107","series-title":"Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science","first-page":"390","article-title":"Real-time logics: complexity and expressiveness","author":"Alur","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib108","series-title":"Proceedings of the 5th Annual Symposium on Logic in Computer Science","first-page":"402","article-title":"Explicit clock temporal logic","author":"Harel","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib109","series-title":"Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing","article-title":"The benefits of relaxing punctuality","author":"Alur","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib110","series-title":"ICALP 90: Automata, Languages and Programming","first-page":"322","article-title":"Automata for modeling real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib111","series-title":"Ph.D. Thesis","article-title":"Techniques for Automatic Verification of Real-Time Systems","author":"Alur","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib112","series-title":"Proceedings at the 5th Conference on Logic in Computer Science, IEEE","article-title":"Model checking for real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib113","series-title":"Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems","article-title":"Quantitative temporal reasoning","author":"Emerson","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib114","series-title":"Ph.D. Thesis","article-title":"Time and Probability in Formal Design and Distributed Systems","author":"Hansson","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib115","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0164-1212(90)90074-V","article-title":"TRIO, a logic language for executable specifications of real-time systems","volume":"12","author":"Ghezzi","year":"1990","journal-title":"J. Syst. Software"},{"key":"10.1016\/0164-1212(92)90045-L_bib116","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib117","series-title":"LNCS 92","article-title":"A Calculus of Communicating Systems","author":"Milner","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib118","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1145\/3318.3322","article-title":"CIRCAL and the representation of communication, concurrency and time","volume":"7","author":"Milne","year":"1985","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"10.1016\/0164-1212(92)90045-L_bib119","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF00268075","article-title":"Specification oriented semantics","volume":"23","author":"Olderog","year":"1986","journal-title":"ACTA Inform."},{"key":"10.1016\/0164-1212(92)90045-L_bib120","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"Timed CSP: theory and practice","author":"Reed","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib121","series-title":"Technical Report CS-R9053","article-title":"Real Time Process Algebra","author":"Baeten","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib122","series-title":"Proceedings IFIP Working Group Conference on Programming Concepts and Methods","first-page":"402","article-title":"ATP: an algebra for timed processes","author":"Nicollin","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib123","series-title":"CONCUR'90","first-page":"263","article-title":"Ccsr: a calculus for communicating shared resources","author":"Gerber","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib124","series-title":"Proceedings of the Real-Time Systems Symposium","article-title":"A proof system for communicating shared resources","author":"Gerber","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib125","series-title":"Proceedings ICALP 86","article-title":"A timed model for communicating sequential processes","author":"Reed","year":"1986"},{"key":"10.1016\/0164-1212(92)90045-L_bib126","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","article-title":"A timed model for communicating sequential processes","volume":"58","author":"Reed","year":"1988","journal-title":"Theoret. Comp. Sci."},{"key":"10.1016\/0164-1212(92)90045-L_bib127","series-title":"Ph.D. thesis","article-title":"Correctness and Communication in Real-Time Systems","author":"Schneider","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib128","series-title":"CONCUR 90","first-page":"401","article-title":"A temporal calculus of communicating systems","author":"Moller","year":"1990"},{"key":"10.1016\/0164-1212(92)90045-L_bib129","series-title":"Proceedings of ICALP 91","article-title":"CCS + time = an interleaving model for real time systems","author":"Yi","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib130","series-title":"Technical Report 5\/91","article-title":"A process Algebra for Timed Systems","author":"Hennessy","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib131","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"LOTOS-like process algebra with urgent or timed interactions","author":"Bolognesi","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib132","series-title":"Ph.D. Thesis","article-title":"Specification and Proof in Real-Time Systems","author":"Davis","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib133","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"An overview and synthesis of timed process algebras","author":"Nicollin","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib134","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"From ATP to timed graphs and hybrid semantics","author":"Nicollin","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib135","article-title":"A graph-theoretic approach for timing analysis and its implementation","volume":"C36","author":"Jahanian","year":"1987","journal-title":"IEEE Trans. Comp."},{"key":"10.1016\/0164-1212(92)90045-L_bib136","series-title":"Proceedings of the 9th Real-Time Systems Symposium, IEEE Computer Society","first-page":"12","article-title":"A Method for verifying properties of modechart specifications","author":"Jahanian","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib137","series-title":"Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","first-page":"36","article-title":"Using higherorder logic for modular specification of real-time distributed systems","author":"MacEwen","year":"1988"},{"key":"10.1016\/0164-1212(92)90045-L_bib138","series-title":"Proceedings of the 9th International Symposium on Protocol Specification, Testing and Verification","article-title":"Design and verification in real-time distributed computing: an introduction to compositional methods","author":"Hooman","year":"1989"},{"key":"10.1016\/0164-1212(92)90045-L_bib139","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"Putting time into proof outlines","author":"Schneider","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib140","doi-asserted-by":"crossref","first-page":"875","DOI":"10.1109\/32.29487","article-title":"Reasoning about time in high-level language software","volume":"SE-15","author":"Shaw","year":"1989","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(92)90045-L_bib141","series-title":"Technical Report","article-title":"he Temporal Logic of Actions","author":"Lamport","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib142","series-title":"Linear Multivariable Control: A Geometric Approach","author":"Wonham","year":"1985"},{"key":"10.1016\/0164-1212(92)90045-L_bib143","series-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","article-title":"From timed to hybrid systems","author":"Maler","year":"1991"},{"key":"10.1016\/0164-1212(92)90045-L_bib144","series-title":"Technical Report 91-1217","article-title":"Derivation of Sequential, Real-Time, Process-Control Programs","author":"Marzullo","year":"1991"}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016412129290045L?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016412129290045L?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,14]],"date-time":"2019-03-14T22:56:49Z","timestamp":1552604209000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/016412129290045L"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,4]]},"references-count":145,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,4]]}},"alternative-id":["016412129290045L"],"URL":"https:\/\/doi.org\/10.1016\/0164-1212(92)90045-l","relation":{},"ISSN":["0164-1212"],"issn-type":[{"value":"0164-1212","type":"print"}],"subject":[],"published":{"date-parts":[[1992,4]]}}}