{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:40:26Z","timestamp":1742600426548,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540610427"},{"type":"electronic","value":"9783540498742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61042-1_54","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:11:32Z","timestamp":1330290692000},"page":"349-368","source":"Crossref","is-referenced-by-count":2,"title":["Reactive EFSMs \u2014 Reactive Promela\/RSPIN"],"prefix":"10.1007","author":[{"given":"Elie","family":"Najm","sequence":"first","affiliation":[]},{"given":"Frank","family":"Olsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"21_CR1","unstructured":"C. Andr\u00e9 and L. Fancelli. A mixed (asynchronous \/ synchronous) implementation of a real-time system. In Euromicro 90, Amsterdam, 1990."},{"key":"21_CR2","first-page":"1270","volume":"79","author":"G. Berry","year":"1991","unstructured":"G. Berry and A. Benveniste. The synchronous approach to reactive and real-time systems. Another Look at Real Time Programming, Proceedings of the IEEE, 79:1270\u20131282, 1991.","journal-title":"Another Look at Real Time Programming, Proceedings of the IEEE"},{"key":"21_CR3","volume-title":"Data-flow synchronous languages. Rapport de recherche 2089","author":"A. Benveniste","year":"1993","unstructured":"Albert Benveniste, Paul Caspi, Paul Le Guernic, and Nicolas Halbwachs. Data-flow synchronous languages. Rapport de recherche 2089, INRIA, Unit\u00e9 de recherche INRIA Sophia-Antipolis, France, October 1993."},{"key":"21_CR4","volume-title":"The sl synchronous language. Rapport de recherche 2510","author":"F. Boussinot","year":"1995","unstructured":"Fr\u00e9d\u00e9ric Boussinot and Robert de Simone. The sl synchronous language. Rapport de recherche 2510, INRIA, Unit\u00e9 de recherche INRIA Sophia-Antipolis, France, Mars 1995."},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"G. Berry. Communicating reactive processes. In Proc. 20th ACM Conf. on Principles of Programming Languages, Charleston, Virginia, 1993.","DOI":"10.1145\/158511.158526"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"G. Berry. The semantics of pure esterel. In Proc Marktoberdorf Intl. Summer School on Program Design Calculi, LNCS, to appear. Springer-Verlag, 1993.","DOI":"10.1007\/978-3-662-02880-3_12"},{"key":"21_CR7","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0169-7552(91)90080-V","volume":"22","author":"G. Berry","year":"1991","unstructured":"G. Berry and G. Gonthier. Incremental development of an hdlc entity in Esterel. Comp. Networks and ISDN Systems, 22:35\u201349, 1991.","journal-title":"Comp. Networks and ISDN Systems"},{"issue":"2","key":"21_CR8","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87\u2013152, 1992.","journal-title":"Science of Computer Programming"},{"key":"21_CR9","volume-title":"Protocol Specification, Testing and Verification, III","author":"S. Budkowski","year":"1983","unstructured":"S. Budkowski and E. Najm. Structured finite state automata, a new approach for modelling distributed communication systems. In H. Rudin and C. H. West, editors, Protocol Specification, Testing and Verification, III. Elsevier Science Publishers B.V (North-Holland), 1983."},{"issue":"4","key":"21_CR10","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1002\/spe.4380210406","volume":"21","author":"F. Boussinot","year":"1991","unstructured":"F. Boussinot. Reactive c: An extension of c to program reactive systems. Software-Practice and Experience, 21(4):401\u2013428, 1991.","journal-title":"Software-Practice and Experience"},{"key":"21_CR11","unstructured":"P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre, a declarative language for programming synchronous systems. In Proceedings of ACM Conference on Principles of Programming Languages, ACM, 1985."},{"key":"21_CR12","unstructured":"Monica Lara de Souza and Robert de Simone. Using po methods for verifying behavioural equivalences. In Proceedings of FORTE'95, pages 59\u201374, October 1995."},{"key":"21_CR13","volume-title":"Rapport SPECTRE C14","author":"J. Fernandez","year":"1989","unstructured":"Jean-Claude Fernandez. Aldebaran: A tool for verification of communicating processes. Rapport SPECTRE C14, Laboratoire de G\u00e9nie Informatique \u2014 Institut IMAG, Grenoble, September 1989."},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"R. Gerth, R. Kuiper, R. Peled, and W. Penczek. A partial order approach to branching time model checking. In Proceedings of ISTCS, pages 330\u2013339, 1995.","DOI":"10.1109\/ISTCS.1995.377038"},{"key":"21_CR15","unstructured":"Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. PhD thesis, UNIVERSITE DE LIEGE, Facult\u00e9 des Sciences Appliqu\u00e9es, 1994."},{"issue":"2","key":"21_CR16","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1109\/TASSP.1986.1164809","volume":"34","author":"P. Guernic Le","year":"1986","unstructured":"P. Le Guernic. Signal, a data-flow oriented language for signal processing. IEEE Trans. ASSP, 34(2):362\u2013374, 1986.","journal-title":"IEEE Trans. ASSP"},{"key":"21_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous Programming of Reactive Systems","author":"N. Halbswachs","year":"1993","unstructured":"N. Halbswachs. Synchronous Programming of Reactive Systems. Kluwer Academic Press, Netherlands, 1993."},{"key":"21_CR18","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Gerhard Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, N.J., first edition, 1991.","edition":"first edition"},{"key":"21_CR19","unstructured":"M. Jourdan, F. Lagnier, P. Raymond, and F. Maraninchi. A multiparadigm language for reactive systems."},{"key":"21_CR20","unstructured":"E. Madelaine. Verification tools from the Concur project. EATCS Bulletin, 47, 1992."},{"key":"21_CR21","unstructured":"E. Madelaine and D. Vergamini. Auto: A verification tool for distributed systems using reduction of finite automata networks. In Proc. FORTE'89 Conference, Vancouver, 1989."},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"D. Peled. Combining partial order reductions with on-the-fly model-checking. In Proceedings of CAV'94, LNCS 818. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_69"},{"key":"21_CR23","unstructured":"G. Plotkin. A structural approach to operational semantics. Technical report, Comput. Sci. Dept., Aarhus Univ., 1981."},{"key":"21_CR24","volume-title":"Auto and autograph","author":"V. Roy","year":"1990","unstructured":"V. Roy and R. de Simone. Auto and autograph. In R. Kurshan, editor, proceedings of Workshop on Computer Aided Verification, New-Brunswick, June 1990. AMS-DIMACS."},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"A. Valmari. A stubborn attack on state explosion. LNCS 531. Springer-Verlag, 1990.","DOI":"10.1090\/dimacs\/003\/04"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"P. Wolper and P. Godefroid. Partial order methods for temporal verification. In Proceedings of Concur'93, LNCS 715. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57208-2_17"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61042-1_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:12:49Z","timestamp":1742598769000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61042-1_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540610427","9783540498742"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-61042-1_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}