{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T07:52:22Z","timestamp":1649058742486},"reference-count":29,"publisher":"Elsevier BV","issue":"1-5","license":[{"start":{"date-parts":[[1989,8,1]],"date-time":"1989-08-01T00:00:00Z","timestamp":617932800000},"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":["Microprocessing and Microprogramming"],"published-print":{"date-parts":[[1989,8]]},"DOI":"10.1016\/0165-6074(89)90127-0","type":"journal-article","created":{"date-parts":[[2003,9,3]],"date-time":"2003-09-03T17:14:48Z","timestamp":1062609288000},"page":"649-656","source":"Crossref","is-referenced-by-count":3,"title":["Mechanizing the verification of real-time discrete systems"],"prefix":"10.1016","volume":"27","author":[{"given":"J.S.","family":"Ostroff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0165-6074(89)90127-0_BIB1","series-title":"Logics of programs","first-page":"1","article-title":"Nonclausal temporal deduction","author":"Abadi","year":"1985"},{"key":"10.1016\/0165-6074(89)90127-0_BIB2","series-title":"Proceedings of ACM SIGOPS 8th annual 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\/0165-6074(89)90127-0_BIB3","article-title":"A computational logic handbook","author":"Boyer","year":"1988"},{"issue":"2","key":"10.1016\/0165-6074(89)90127-0_BIB4","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 Transactions on Automatic Control"},{"key":"10.1016\/0165-6074(89)90127-0_BIB5","series-title":"Temporal logics and their applications","year":"1987"},{"key":"10.1016\/0165-6074(89)90127-0_BIB6","article-title":"A compositional proof-system for an OCCAM-like real-time language","author":"Hoofman","year":"1987"},{"key":"10.1016\/0165-6074(89)90127-0_BIB7","series-title":"Proceedings of ACM Symposium on Principles of Programming Languages","article-title":"Constraint logic programming","author":"Jaffar","year":"1987"},{"issue":"9","key":"10.1016\/0165-6074(89)90127-0_BIB8","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 Transactions on Software Engineering"},{"key":"10.1016\/0165-6074(89)90127-0_BIB9","series-title":"Proceedings 9th Real-time Systems Symposium","first-page":"12","article-title":"A method for verifying properties of modechart specifications","author":"Jahanian","year":"1988"},{"key":"10.1016\/0165-6074(89)90127-0_BIB10","series-title":"0roc. 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\/0165-6074(89)90127-0_BIB11","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-15648-8_14","article-title":"Compositional Semantics for Real-time Distributed Computing","author":"Koymans","year":"1985"},{"key":"10.1016\/0165-6074(89)90127-0_BIB12","first-page":"36","article-title":"Timed acceptances: a model of time dependent processes","volume":"LNCS 331","author":"Lee","year":"1988"},{"issue":"3","key":"10.1016\/0165-6074(89)90127-0_BIB13","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1109\/TSE.1987.233170","article-title":"Safety analysis using Petrinets","volume":"SE-13","author":"Leveson","year":"1987","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/0165-6074(89)90127-0_BIB14","series-title":"Abstracts of the IEEE Computer Society: 4th Workshop on real-time operating systems","first-page":"125","article-title":"Expressing requirements for distributed real-time systems","author":"MacEwen","year":"1987"},{"key":"10.1016\/0165-6074(89)90127-0_BIB15","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\/0165-6074(89)90127-0_BIB16","series-title":"International workshop on timed Petri nets","first-page":"162","article-title":"PAREDE: An automated tool for the analysis of time(d) Petri nets","author":"Menasche","year":"1985"},{"key":"10.1016\/0165-6074(89)90127-0_BIB17","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","article-title":"Recoverability of communication protocols - implications of a theoretical study","author":"Merlin","year":"1976","journal-title":"IEEE Transactions on Communications"},{"issue":"2","key":"10.1016\/0165-6074(89)90127-0_BIB18","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 Transactions on Programming Languages and Systems"},{"issue":"2","key":"10.1016\/0165-6074(89)90127-0_BIB19","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\/0165-6074(89)90127-0_BIB20","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\/0165-6074(89)90127-0_BIB21","series-title":"Software for Computer Control 1988 (Selected papers from 5th IFAC\/IFIP Symposium SOCOCO'88), IFAC Proceeding Series, Number 2","first-page":"15","article-title":"Modularity in the ESM\/RTL framework","author":"Ostroff","year":"1989"},{"key":"10.1016\/0165-6074(89)90127-0_BIB22","article-title":"Temporal Logic for Real-Time Systems","author":"Ostroff","year":"1989"},{"key":"10.1016\/0165-6074(89)90127-0_BIB23","series-title":"Proceedings of 9th IEEE International Conference on Distributed Computing Systems","article-title":"Verification of finite state real-time distributed processes","author":"Ostroff","year":"1989"},{"key":"10.1016\/0165-6074(89)90127-0_BIB24","series-title":"Proceedings of the 8th IEEE Real-Time Systems Symposium","first-page":"124","article-title":"Modelling, specifying and verifying real-time embedded computer systems","author":"Ostroff","year":"1987"},{"key":"10.1016\/0165-6074(89)90127-0_BIB25","series-title":"Proceedings of the 26th IEEE Conference on Decision and Control","first-page":"681","article-title":"State machines, temporal logic and control: a framework for discrete event systems","author":"Ostroff","year":"1987"},{"key":"10.1016\/0165-6074(89)90127-0_BIB26","series-title":"Current trends in concurrency","article-title":"Application of temporal logic to the specification and verification of reactive systems: a survey of current trends","author":"Pnueli","year":"1986"},{"key":"10.1016\/0165-6074(89)90127-0_BIB27","series-title":"Proceedings of 4th International Workshop on Protocol Verification and Testing","article-title":"Performance analysis of timed Petri nets","author":"Razouk","year":"1984"},{"key":"10.1016\/0165-6074(89)90127-0_BIB28","series-title":"Proceedings ICALP 86","article-title":"A timed model for communicating sequential processes","author":"Reed","year":"1986"},{"key":"10.1016\/0165-6074(89)90127-0_BIB29","series-title":"Proceedings 7th Annual Symposium on Computer Architecture","article-title":"Timed Petri nets and preliminary performance evaluation","author":"Zubrek","year":"1980"}],"container-title":["Microprocessing and Microprogramming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0165607489901270?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0165607489901270?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T09:56:56Z","timestamp":1551088616000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0165607489901270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,8]]},"references-count":29,"journal-issue":{"issue":"1-5","published-print":{"date-parts":[[1989,8]]}},"alternative-id":["0165607489901270"],"URL":"https:\/\/doi.org\/10.1016\/0165-6074(89)90127-0","relation":{},"ISSN":["0165-6074"],"issn-type":[{"value":"0165-6074","type":"print"}],"subject":[],"published":{"date-parts":[[1989,8]]}}}