{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T18:30:26Z","timestamp":1675794626092},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Journal of Real-Time Systems"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1007\/bf00365462","type":"journal-article","created":{"date-parts":[[2004,11,2]],"date-time":"2004-11-02T13:03:06Z","timestamp":1099400586000},"page":"5-35","source":"Crossref","is-referenced-by-count":20,"title":["A verifier for real-time properties"],"prefix":"10.1007","volume":"4","author":[{"given":"J. S.","family":"Ostroff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"51","volume-title":"Protocol Specification, Testing and Verification, III","author":"S. Aggarwal","year":"1983","unstructured":"S.Aggarwal and R.P.Kurshan. 1983. Modelling Elapsed Time in Protocol Specifications. In H.Rudin and C.West, (eds.), Protocol Specification, Testing and Verification, III, pp. 51?62. IBM Research, North-Holland, June."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D.L. Dill. 1990. Model Checking for Real-Time Systems. In Proceedings 5th Conference on Logic in Computer Science. IEEE.","DOI":"10.1109\/LICS.1990.113766"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Rajeev Alur and Thomas Henzinger. 1990. Real-Time Logics: Complexity and Expressiveness. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pp. 390?401, June.","DOI":"10.21236\/ADA323441"},{"issue":"3","key":"CR4","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"B.Berthomieu and MichaelDiaz. 1991. Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Transactions on Software Engineering, 17,(3): 259?273, March.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"CR5","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1109\/32.4651","volume":"14","author":"J. Billington","year":"1988","unstructured":"J.Billington, G.R.Wheeler, and M.C.Wilbur-Ham. 1988. PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols. IEEE Transactions on Software Engineering, 14(3): 301?316, March.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. 1988. Parallel Program Design. Addison-Wesley.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"issue":"2","key":"CR7","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M.Clarke, E.A.Emerson, and A.P.Sistla. 1986. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic. ACM Transactions on Programming Languages and Systems, 8(2): 244?263, April.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D.Harel. 1987. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8: 231?274.","journal-title":"Science of Computer Programming"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"D.Harel, H.Lachover, A.Naamad, A.Pnueli, M.Politi, R.Sherman, and M.Trachtenbrot. 1990. Statemate: a Working Environment for the Development of Complex Reactive Systems. IEEE Transactions on Software Engineering, 16: 403?414.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"E. Harel, O. Lichtenstein, and A. Pnueli. 1990. Explicit Clock Temporal Logic. In Proceedings of the 5th Annual Symposium on Logic in Computer Science, pp. 402?413, June.","DOI":"10.1109\/LICS.1990.113765"},{"issue":"9","key":"CR11","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","volume":"12","author":"F. Jahanian","year":"1986","unstructured":"F.Jahanian and A.K.Mok. 1986. Safety Analysis of Timing Properties in Real-Time Systems. IEEE Transactions on Software Engineering, SE-12(9): 890?904, September.","journal-title":"IEEE Transactions on Software Engineering, SE"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"F. Jahanian and A.K. Mok. 1987. A Graph-Theoretic Approach for Timing Analysis and Its Implementation. IEEE Transactions on Computer, C36(8).","DOI":"10.1109\/TC.1987.5009519"},{"key":"CR13","unstructured":"F. Jahanian and D. Stuart. 1988. A Method for Verifying Properties of Modechart Specifications. In Proceedings 9th Real-time Systems Symposium, pp. 12?21. IEEE Computer Society, December."},{"issue":"4","key":"CR14","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"Ron Koymans","year":"1990","unstructured":"RonKoymans. 1990. Specifying Real-Time Properties With Metric Temporal Logic. Real-Time Systems, 2(4): 255?299, November.","journal-title":"Real-Time Systems"},{"issue":"3","key":"CR15","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1109\/TSE.1987.233170","volume":"13","author":"N.G. Leveson","year":"1987","unstructured":"N.G.Leveson and J.L.Stolzy. 1987. Safety Analysis Using Petri Nets. IEEE Transactions on Software Engineering, SE-13(3): 386?397, March.","journal-title":"IEEE Transactions on Software Engineering, SE"},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. 1985. Checking that Finite State Concurrent Programs Satisfy Their Linear Specifications. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pp. 97?105.","DOI":"10.1145\/318593.318622"},{"key":"CR17","unstructured":"J.S. Ostroff. 1987. Real-Time Computer Control of Discrete Event Systems Modelled by Extended State Machines: A Temporal Logic Approach. Technical Report 8618, Systems Control Group, Dept. of Electrical Engineering, University of Toronto, September 1986. Revised January 1987."},{"key":"CR18","series-title":"Advanced Software Development Series","volume-title":"Temporal Logic for Real-Time Systems","author":"J.S. Ostroff","year":"1989","unstructured":"J.S.Ostroff. 1989. Temporal Logic for Real-Time Systems. Advanced Software Development Series. Research Studies Press Limited (distributed by John Wiley and Sons), Taunton, England."},{"issue":"2","key":"CR19","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/71.80145","volume":"1","author":"J.S. Ostroff","year":"1990","unstructured":"J.S.Ostroff. 1990. Deciding Properties of Timed Transition Models. IEEE Transactions on Parallel and Distributed Systems, 1(2): 170?183, April.","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"J.S. Ostroff. 1990. A Logic for Real-Time Discrete Event Processes. IEEE Control Systems Magazine, June.","DOI":"10.1109\/37.56283"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"J.S. Ostroff and W.M. Wonham. 1990. A Framework for Real-Time Discrete Event Control. IEEE Transactions on Automatic Control, April.","DOI":"10.1109\/9.52290"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. 1986. Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. In J. de Bakker, W.P. de Roever, and G. Rozenburg, (eds.) Current Trends in Concurrency, LNCS 244. Springer-Verlag, 1986.","DOI":"10.1007\/BFb0027047"}],"container-title":["Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00365462.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00365462\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00365462","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T17:47:42Z","timestamp":1585936062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00365462"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF00365462"],"URL":"https:\/\/doi.org\/10.1007\/bf00365462","relation":{},"ISSN":["0922-6443","1573-1383"],"issn-type":[{"value":"0922-6443","type":"print"},{"value":"1573-1383","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}