{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T08:33:01Z","timestamp":1718699581298},"reference-count":53,"publisher":"Elsevier BV","issue":"5","license":[{"start":{"date-parts":[[2002,11,1]],"date-time":"2002-11-01T00:00:00Z","timestamp":1036108800000},"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":["Computer Standards & Interfaces"],"published-print":{"date-parts":[[2002,11]]},"DOI":"10.1016\/s0920-5489(02)00066-1","type":"journal-article","created":{"date-parts":[[2002,10,3]],"date-time":"2002-10-03T19:36:32Z","timestamp":1033673792000},"page":"395-409","source":"Crossref","is-referenced-by-count":0,"title":["Evaluating real-time software specification languages"],"prefix":"10.1016","volume":"24","author":[{"given":"Dong-Tsan","family":"Lee","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0920-5489(02)00066-1_BIB1","series-title":"Rexworkshop Mook, The Netherlands, June 1991, LNCS 600","first-page":"74","article-title":"Logics and models of real-time: a survey, in: real-time: theory in practice","author":"Alur","year":"1992"},{"issue":"9","key":"10.1016\/S0920-5489(02)00066-1_BIB2","first-page":"11","article-title":"RT-ASLAN: a specification language for real-time systems","volume":"12","author":"Auernheimer","year":"1986","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"10.1016\/S0920-5489(02)00066-1_BIB3","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/349194.349197","article-title":"Temporal logics for real-time system specification","volume":"32","author":"Bellini","year":"2000","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB4","doi-asserted-by":"crossref","DOI":"10.1145\/800216.806585","article-title":"Proving real-time properties of programs with temporal logic","author":"Bernstein","year":"1981"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB5","series-title":"Real-Time: Theory in Practice LNCS 600","first-page":"124","article-title":"Timed process algebra with urgent interactions and a unique powerful binary operator","author":"Bolognesi","year":"1992"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB6","series-title":"The Unified Modeling Language User Guide","author":"Booch","year":"1999"},{"issue":"9","key":"10.1016\/S0920-5489(02)00066-1_BIB7","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1109\/32.629494","article-title":"Specification of real-time systems using ASTRAL","volume":"23","author":"Coen-Porisini","year":"1997","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB8","series-title":"Symbolic Logic and Mechanic Theorem Proving","author":"Chang","year":"1973"},{"issue":"1","key":"10.1016\/S0920-5489(02)00066-1_BIB9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1142\/S0218194097000023","article-title":"Formal requirements and design specifications: the clepsydra methodology","volume":"7","author":"Ciaccia","year":"1997","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB10","series-title":"Real-Time: Theory in Practice LNCS 600","article-title":"Timed CSP: theory and practice","author":"Davies","year":"1992"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB11","series-title":"Specification and Proof in Real-Time CSP","author":"Davies","year":"1993"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB12","series-title":"Structured Analysis and System Specification","author":"DeMarco","year":"1978"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB13","series-title":"Real-Time UML: Developing Efficient Objects for Embedded Systems","author":"Douglass","year":"1998"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB14","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1109\/52.582979","article-title":"A formal method for building concurrent real-time software","author":"Fidge","year":"1997","journal-title":"IEEE Software"},{"issue":"5","key":"10.1016\/S0920-5489(02)00066-1_BIB15","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/103167.103173","article-title":"Multilevel specification of real-time systems","volume":"34","author":"Gabrielian","year":"1991","journal-title":"CACM"},{"issue":"2","key":"10.1016\/S0920-5489(02)00066-1_BIB16","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":"Journal of Systems and Software"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB18","series-title":"Advances in Linear Logic","article-title":"Linear logic: its syntax and semantics","author":"Girard","year":"1995"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB19","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":"Science of Computer Programming"},{"issue":"5","key":"10.1016\/S0920-5489(02)00066-1_BIB20","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1145\/42411.42414","article-title":"On visual formalisms","volume":"31","author":"Harel","year":"1988","journal-title":"Communications of the ACM"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB21","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1109\/2.596624","article-title":"Executable object modelling with statechart","author":"Harel","year":"1997","journal-title":"Computer"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB22","series-title":"Strategies for Real-Time System Specification","author":"Hatley","year":"1987"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB23","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB24","series-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft","year":"1979"},{"issue":"12","key":"10.1016\/S0920-5489(02)00066-1_BIB25","doi-asserted-by":"crossref","first-page":"879","DOI":"10.1109\/32.368134","article-title":"Modechart: a specification language for real-time systems","volume":"20","author":"Jahanian","year":"1994","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2\u20133","key":"10.1016\/S0920-5489(02)00066-1_BIB26","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1049\/ip-sen:19986036","article-title":"Visualising action contracts in object-oriented modeling","volume":"145","author":"Kent","year":"1998","journal-title":"IEE Proceedings. Software"},{"issue":"4","key":"10.1016\/S0920-5489(02)00066-1_BIB27","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying real-time properties with metri temporal logic","volume":"2","author":"Koymans","year":"1990","journal-title":"Real-Time Systems"},{"issue":"6","key":"10.1016\/S0920-5489(02)00066-1_BIB28","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/2.294859","article-title":"Real time: further misconceptions (or half truths)","volume":"27","author":"Kurki-Suonio","year":"1994","journal-title":"Computer"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB29","series-title":"Real-Time Systems Design and Analysis: an Engineer's Handbook","author":"Laplante","year":"1997"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB30","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1111\/j.1551-6708.1987.tb00863.x","article-title":"Why a diagram is (sometimes) worth a ten thousands words","volume":"11","author":"Larkin","year":"1987","journal-title":"Cognitive Science"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB31","series-title":"UML for Real-Time Overview","author":"Lyons","year":"1998"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB32","unstructured":"D.T. Lee, Modeling real-time systems with linear logic, Technical Report, Oct. 2000."},{"key":"10.1016\/S0920-5489(02)00066-1_BIB33","series-title":"The Temporal Logic of Reactive and Concurrent System-Specification","author":"Manna","year":"1991"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB34","series-title":"Elementary Computability, Formal Languages, and Automata","author":"McNaughton","year":"1983"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB35","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB36","series-title":"Processings of CONCUR'90, LNCS 458","first-page":"401","article-title":"A temporal calculus of communicating systems","author":"Moller","year":"1990"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB37","series-title":"Automata, Languages, and Programming, LNCS 623","first-page":"559","article-title":"Behavioural abstraction in TCCS","author":"Moller","year":"1992"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB38","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/0950-5849(95)01049-1","article-title":"Using timed CSP during object oriented design of real-time systems","volume":"38","author":"O'Donoghue","year":"1996","journal-title":"Information and Software Technology"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB39","series-title":"Structured System Development","author":"Orr","year":"1977"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB40","series-title":"Temporal Logic for Real-Time Systems","author":"Ostroff","year":"1989"},{"issue":"1","key":"10.1016\/S0920-5489(02)00066-1_BIB41","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/0164-1212(92)90045-L","article-title":"Formal methods for the specification and design of real-time safety critical systems","volume":"18","author":"Ostroff","year":"1992","journal-title":"Journal of Systems and Software"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB42","series-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 331","first-page":"84","article-title":"Applications of temporal logic to the specification of real-time systems","author":"Pnueli","year":"1988"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB43","series-title":"Real-Time Object-Oriented Modeling","author":"Selic","year":"1994"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB44","series-title":"Using UML for Modeling Complex Real-Time Systems","author":"Selic","year":"1998"},{"issue":"3","key":"10.1016\/S0920-5489(02)00066-1_BIB45","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1109\/32.667880","article-title":"Extending statecharts with temporal logic","volume":"24","author":"Sowmya","year":"1998","journal-title":"IEEE Transaction on Software Engineering"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB46","series-title":"The Z Notation: a Reference Manual","author":"Spivey","year":"1992"},{"issue":"42","key":"10.1016\/S0920-5489(02)00066-1_BIB47","first-page":"230","article-title":"On computable numbers with an application to the Entscheidungsproblem","volume":"2","author":"Turing","year":"1936","journal-title":"Proceedings of the London Mathematical Society"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB48","series-title":"Logical Construction of Programs","author":"Warnier","year":"1974"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB49","series-title":"Research Directions in Concurrent Object-Oriented Programming","article-title":"Tradeoffs between reasoning and modeling","author":"Wegner","year":"1993"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB50","series-title":"Handbook of Computer Science and Engineering","article-title":"Interactive software technology","author":"Wegner","year":"1996"},{"issue":"5","key":"10.1016\/S0920-5489(02)00066-1_BIB51","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/253769.253801","article-title":"Why interaction is more powerful than algorithms","volume":"40","author":"Wegner","year":"1997","journal-title":"Communications of the ACM"},{"issue":"2","key":"10.1016\/S0920-5489(02)00066-1_BIB52","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/S0304-3975(97)00154-0","article-title":"Interactive foundation of computing","volume":"192","author":"Wegner","year":"1998","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S0920-5489(02)00066-1_BIB53","series-title":"LNCS 1565","first-page":"100","article-title":"Interaction as a framework for modeling","author":"Wegner","year":"1999"}],"container-title":["Computer Standards & Interfaces"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0920548902000661?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0920548902000661?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,10]],"date-time":"2019-04-10T18:29:23Z","timestamp":1554920963000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0920548902000661"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,11]]},"references-count":53,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2002,11]]}},"alternative-id":["S0920548902000661"],"URL":"https:\/\/doi.org\/10.1016\/s0920-5489(02)00066-1","relation":{},"ISSN":["0920-5489"],"issn-type":[{"value":"0920-5489","type":"print"}],"subject":[],"published":{"date-parts":[[2002,11]]}}}