{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T15:02:18Z","timestamp":1694617338874},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1999,12,1]],"date-time":"1999-12-01T00:00:00Z","timestamp":944006400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1999,12]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>We present in this paper some new language features and constructs, that allow the joint synchronous\/asynchronous programming of reactive applications, as well as their formal verification.<\/jats:p>\n          <jats:p>\n            We show that reactive applications may be dealt with from two points of view. First, from the\n            <jats:sc>chronological<\/jats:sc>\n            point of view, i.e., when reactions are instantaneous, generated by event occurrences in discrete time. Second, from the\n            <jats:sc>chronometrical<\/jats:sc>\n            point of view, when reactions have durations in dense time. This duality must be expressible in languages that allow a consistent programming of both\n            <jats:sc>synchronous<\/jats:sc>\n            and\n            <jats:sc>asynchronous<\/jats:sc>\n            features. The objective of mixing these dual approaches leads to model reactive systems by using\n            <jats:sc>hybrid systems<\/jats:sc>\n            , to deal simultaneously with both discrete and continuous phenomena. Furthermore, this must be followed by some verification of the application's properties, with respect to its behavioural and quantitative features.\n          <\/jats:p>\n          <jats:p>\n            We analyze several existing frameworks that meet these requirements, and propose our own approach based on the language E\n            <jats:italic>lectre<\/jats:italic>\n            .\n          <\/jats:p>","DOI":"10.1007\/s001650050042","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T06:53:02Z","timestamp":1030258382000},"page":"448-471","source":"Crossref","is-referenced-by-count":1,"title":["Hybrid Verifications of Reactive Programs"],"prefix":"10.1145","volume":"11","author":[{"given":"Olivier","family":"Roux","sequence":"first","affiliation":[{"name":"IRCyN, CNRS and Ecole Centrale de Nantes, France, , , , , , FR"}]},{"given":"Vlad","family":"Rusu","sequence":"additional","affiliation":[{"name":"Iri sa, Rennes cedex, France, , , , , , FR"}]},{"given":"Franck","family":"Cassez","sequence":"additional","affiliation":[{"name":"IRCyN, CNRS and Ecole Centrale de Nantes, France, , , , , , FR"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"World Scientific Pub.","author":"Arnold A.","year":"1994"},{"key":"p_2","volume-title":"Proc. IEEE 5th Symp. Logic in Computer Science, LNCS","author":"Alur R.","year":"1990"},{"key":"p_3","volume-title":"Theoretical Computer Science B","author":"Alur R.","year":"1995"},{"key":"p_4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","article-title":"The algorithmic analysis of hybrid systems","volume":"138","author":"Alur R.","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"p_5","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Al","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"p_6","volume-title":"Automatic symbolic verification of embedded systems. Technical report","author":"Alur R.","year":"1994"},{"key":"p_7","first-page":"221","volume-title":"Proceedings of the IJCAI'81","author":"All","year":"1981"},{"key":"p_8","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/BF01898401","article-title":"Real time process algebra","volume":"3","author":"Ba","year":"1991","journal-title":"Formal Aspects of Computing"},{"issue":"9","key":"p_9","doi-asserted-by":"crossref","first-page":"1270","DOI":"10.1109\/5.97297","article-title":"The synchronous approach to reactive and real-time systems","volume":"79","author":"Be","year":"1991","journal-title":"Proceedings of the IEEE"},{"key":"p_10","volume-title":"2nd International Workshop on Formal Design of Safety Critical Embedded Systems (FEMSYS'99)","author":"Beaufreton P.","year":"1999"},{"key":"p_11","volume-title":"International Workshop on Hybrid and Real-Time Systems","volume":"1201","author":"Boniol F.","year":"1997"},{"issue":"4","key":"p_12","first-page":"156","article-title":"The sl synchronous language","volume":"22","author":"Bo","year":"1996","journal-title":"IEEE Transactions on Software Engineering"},{"key":"p_13","volume-title":"Ecole des mines, CMA, Sophia-Antipolis","author":"Ber","year":"1989"},{"key":"p_14","volume-title":"Proc. 13th Conference on Foundations of Software Technology and Theoretical Computer Science","volume":"761","author":"Ber","year":"1993"},{"issue":"2","key":"p_15","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","article-title":"The Esterel synchronous language: design, semantics, and implementation","volume":"19","author":"Be","year":"1992","journal-title":"Science of Computer Programming"},{"key":"p_16","volume-title":"LNCS","author":"Bengtsson J.","year":"1996"},{"key":"p_17","volume-title":"Proc. of the Euro-Par'97 Workshop on Real-Time Systems and Constraints","author":"Bu","year":"1997"},{"key":"p_18","first-page":"85","volume-title":"Proc. 20th ACM Symposium on Principle of Programming Languages (POPL)","author":"Berry G.","year":"1993"},{"key":"p_20","doi-asserted-by":"crossref","unstructured":"[CBE85] \n      Clarke E. M. Browne M. C. Emerson E. A.\n     and \n      Sistla A. P\n  .: \n  Using temporal logic for automatic verification of finite state systems volume \n  13\n   of \n  Proceedings of the NATO Advanced Study Institute on Logics and Models of Concurrent Systems pages \n  3\n  -\n  26\n  . \n  Springer Verlag 1985\n  .","DOI":"10.1007\/978-3-642-82453-1_1"},{"key":"p_21","volume-title":"3rd. Computer-Aided Verification (CAV'92)","author":"Courcoubetis C.","year":"1992"},{"key":"p_22","volume-title":"Parallel Program Design: a foundation","author":"Ch","year":"1988"},{"issue":"1","key":"p_23","first-page":"109","article-title":"Compilation of the Electre reactive language into finite transition systems","volume":"146","author":"Ca","year":"1995","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"p_24","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":"Har","year":"1987","journal-title":"Science of Computer Programming"},{"issue":"9","key":"p_25","doi-asserted-by":"crossref","first-page":"1304","DOI":"10.1109\/5.97300","article-title":"The synchronous dataflow language Lustre","volume":"79","author":"Halbwachs N.","year":"1991","journal-title":"Proceedings of the IEEE"},{"key":"p_26","volume-title":"Proc. of the 11th Annual Symposium on Logic in Computer Science, LICS'96. IEEE Computer Society Press","author":"Hen","year":"1996"},{"key":"p_27","volume-title":"Proc. 1st. Workshop on Tools and Algorithms for the Analisys of Systems, LNCS","author":"Henzinger T. A.","year":"1994"},{"key":"p_28","volume-title":"Symbolic model-checking for real-time systems. Information and Computation, (111)","author":"Henzinger T. A.","year":"1994"},{"issue":"8","key":"p_29","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating sequential processes","volume":"21","author":"Hoa","year":"1978","journal-title":"Communications of the ACM"},{"issue":"8","key":"p_30","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating sequential processes","volume":"21","author":"Hoa","year":"1978","journal-title":"Communications of the ACM"},{"key":"p_31","first-page":"477","volume-title":"Logics and Models of Concurrent Systems","author":"Ha","year":"1985"},{"key":"p_32","volume-title":"International Symposium on Static Analysis, LNCS","author":"Halbwachs N.","year":"1994"},{"key":"p_33","first-page":"54","volume-title":"2nd IEEE Symposium on Logic in Computer Science","author":"Harel D.","year":"1987"},{"issue":"3","key":"p_34","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lam","year":"1994","journal-title":"ACM Transactions On Programming Languages and Systems"},{"issue":"9","key":"p_35","doi-asserted-by":"crossref","first-page":"1321","DOI":"10.1109\/5.97301","article-title":"Programming real-time applications with Signal","volume":"79","author":"Le Guernic P.","year":"1991","journal-title":"Proceedings of the IEEE"},{"key":"p_36","volume-title":"A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science","author":"Mil","year":"1980"},{"key":"p_37","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1007\/BF01191722","article-title":"Models for reactivity","volume":"30","author":"Ma","year":"1993","journal-title":"Acta Informatica"},{"key":"p_38","doi-asserted-by":"crossref","unstructured":"[\n      Pn\n    H88] Pnueli A. and \n      Harel E\n  .: \n  Application of Temporal Logic to the Specification of Reactive Systems volume \n  331\n   of \n  Lecture Notes in Computer Science pages \n  84\n  -\n  98\n  . \n  Springer Verlag Warwick\n   (United Kingdom) 1988\n  .","DOI":"10.1007\/3-540-50302-1_4"},{"key":"p_39","volume-title":"A structural approach to operational semantics. Research Report DAIMI FN-19","author":"Plo D.","year":"1981"},{"issue":"1","key":"p_40","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(92)90388-V","article-title":"Operational semantics of a kernel of the language Electre","volume":"97","author":"Perraud J.","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"p_41","volume-title":"Le langage r\u00e9actif asynchrone Electre. Technique et Science Informatiques (TSI), 11(5):35-66","author":"Roux O.","year":"1992"},{"key":"p_42","first-page":"28","volume-title":"Proc. of the ACM SIGPLAN Workshop on Language, Compiler and Tool Support for Real-Time Systems","author":"Ru","year":"1994"},{"key":"p_43","volume-title":"Proc. of 7th Euromicro Workshop on Real-Time Systems","author":"Ru","year":"1995"},{"key":"p_44","volume-title":"Proc. Workshop on Real-Time and Hybrid Systems","author":"Ro","year":"1995"},{"key":"p_45","first-page":"295","volume-title":"Proc. Euromicro Workshop on Real-Time Systems","author":"Ri","year":"1996"},{"key":"p_46","volume-title":"International Static Analysis Symposium","volume":"1145","author":"Ro","year":"1996"},{"key":"p_47","volume-title":"Th\u00e8se de Doctorat","author":"Rus","year":"1996"},{"key":"p_48","volume-title":"7th International Conference on Algebraic Methodology and Software Technology (AMAST'98)","volume":"1548","author":"Gr\u00e9goire Sutre","year":"1999"},{"key":"p_49","first-page":"225","volume-title":"Proc. Algebraic Methodology And Software Technology (AMAST'93)","author":"Shy","year":"1993"},{"key":"p_50","doi-asserted-by":"crossref","unstructured":"[\n      Sh\n    R94] Shyamasundar R. K. and \n      Ramesh S\n  .: \n  Languages for Reactive Specifications: Synchrony Vs Asynchrony volume \n  863\n   of \n  Lecture Notes in Computer Science pages \n  621\n  -\n  640\n  . \n  Springer Verlag September \n  1994\n  .","DOI":"10.1007\/3-540-58468-4_187"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050042.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050042\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050042","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:33:12Z","timestamp":1641483192000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050042"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,12]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1999,12]]}},"alternative-id":["10.1007\/s001650050042"],"URL":"https:\/\/doi.org\/10.1007\/s001650050042","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,12]]}}}