{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:26Z","timestamp":1725490226664},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665878"},{"type":"electronic","value":"9783540481195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48119-2_19","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T21:23:00Z","timestamp":1188336180000},"page":"307-327","source":"Crossref","is-referenced-by-count":23,"title":["If: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[]},{"given":"Jean-Claude","family":"Fernandez","sequence":"additional","affiliation":[]},{"given":"Lucian","family":"Ghirvu","sequence":"additional","affiliation":[]},{"given":"Susanne","family":"Graf","sequence":"additional","affiliation":[]},{"given":"Jean-Pierre","family":"Krimm","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Mounier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"19_CR1","unstructured":"Telelogic AB. SDT Reference Manual. http:\/\/www.telelogic.se\/solution\/tools\/sdt.asp , 1993."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D.L. Dill. Model Checking in Dense Real Time. Information and Computation, 104(1), 1993.","DOI":"10.1006\/inco.1993.1024"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. ISDN, 14(1), jan 1988.","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"D. Bo\u015dna\u0109ki and D. Dams. Integrating Real Time into Spin: A Prototype Implementation. In Proceedings of the FORTE\/PSTV XVIII Conference, 1998.","DOI":"10.1007\/978-0-387-35394-4_26"},{"key":"19_CR5","unstructured":"D. Bo\u015dna\u0109ki, D. Dams, L. Holenderski, and N. Sidorova. Verifying the MASCARA Protocol in SPIN. submitted to the SPIN\u201999 Workshop, mai 1999."},{"key":"19_CR6","unstructured":"M. Bozga, J-C. Fernandez, L. Ghirvu, S. Graf, L. Mounier, J.P. Krimm, and J. Sifakis. The Intermediate Representation IF. Technical report, Verimag, 1998."},{"key":"19_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of SAS\u201999, Venezia, Italy","author":"M. Bozga","year":"1999","unstructured":"M. Bozga, J.-C. Fernandez, and L. Ghirvu. State Space Reduction based on Live Variables Analysis. In Proceedings of SAS\u201999, Venezia, Italy, LNCS, September 1999. to appear."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"M. Bozga, J.-C. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, and J. Sifakis. IF: An Intermediate Representation for SDL and its Applications. In Proceedings of SDL-FORUM\u201999, Montreal, Canada, June 1999.","DOI":"10.1016\/B978-044450228-5\/50028-X"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J.-C. Fernandez, and N. Halbwachs. Minimal Model Generation. In Proceedings of CAV\u201990, Rutgers, New Jersey, volume 3 of DIMACS, pages 85\u201392, June 1990.","DOI":"10.1090\/dimacs\/003\/08"},{"issue":"1+2","key":"19_CR10","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/s100090050012","volume":"1","author":"M. Bozga","year":"1997","unstructured":"M. Bozga, J.-C. Fernandez, A. Kerbrat, and L. Mounier. Protocol Verification with the Aldebaran Toolset. STTT, 1(1+2):166\u2013183, December 1997.","journal-title":"STTT"},{"key":"19_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u201998","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing Abstractions of Infinite State Systems Compositionally and Automatically. In Proceedings of CAV\u201998, Vancouver, Canada, volume 1427 of LNCS, June 1998."},{"key":"19_CR12","unstructured":"J.A. Bergstra, C.A. Middelburg, and Y.S. Usenko. Discrete Time Process Algebra and the Semantics of SDL. Technical Report SEN-R9809, CWI, June 1998."},{"key":"19_CR13","unstructured":"M. Bozga. SMI: An Open Toolbox for Symbolic Protocol Verification. Technical Report 97-10, Verimag, Sep 1997."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"M. Broy. Towards a Formal Foundation of the Specification and Description Language SDL. Formal Aspects on Computing, 1991.","DOI":"10.1007\/BF01211434"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computation, 35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"19_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5_5","volume-title":"International Symposium: Compositionality-The Significant Difference, Holstein, Germany","author":"S. Bornot","year":"1998","unstructured":"S. Bornot, J. Sifakis, and S. Tripakis. Modeling Urgency in Timed Systems. In International Symposium: Compositionality-The Significant Difference, Holstein, Germany, volume 1536 of LNCS, 1998."},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"E. Chang and R. Roberts. An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes. Communications of ACM, 22(5), 1979.","DOI":"10.1145\/359104.359108"},{"key":"19_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TACAS\u201996","author":"C. Courcoubetis","year":"1996","unstructured":"C. Courcoubetis and S. Tripakis. Extending Promela and Spin for Real Time. In Proceedings of TACAS\u201996, volume 1055 of LNCS, 1996."},{"key":"19_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u201996, New Brunswick, USA","author":"J.-C. Fernandez","year":"1996","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox. In Proceedings of CAV\u201996, New Brunswick, USA, volume 1102 of LNCS, July 1996."},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"J.-C. Fernandez, C. Jard, T. J\u00e9ron, and C. Viho. An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology. SCP, 29, 1997.","DOI":"10.1016\/S0167-6423(96)00032-9"},{"key":"19_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u201993, Heraklion, Greece","author":"J.-C. Fernandez","year":"1993","unstructured":"J.-C. Fernandez, A. Kerbrat, and L. Mounier. Symbolic Equivalence Checking. In Proceedings of CAV\u201993, Heraklion, Greece, volume 697 of LNCS, 1993."},{"key":"19_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TACAS\u201998, Lisbon, Portugal","author":"H. Garavel","year":"1998","unstructured":"H. Garavel. OPEN\/\u00c6SAR: An Open Software Architecture for Verification, Simulation, and Testing. In Proceedings of TACAS\u201998, Lisbon, Portugal, volume 1384 of LNCS, 1998."},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"S. Graf, G. L\u00fcttgen, and B. Steffen. Compositional Minimisation of Finite State Systems using Interface Specifications. Formal Aspects of Computation, 3, 1996.","DOI":"10.1007\/BF01211911"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"H. Garavel and L. Mounier. Specification and Verification of Distributed Leader Election Algorithms for Unidirectional Ring Networks. SCP, 29, 1997.","DOI":"10.1016\/S0167-6423(96)00034-2"},{"key":"19_CR25","unstructured":"J.C. Godskesen. An Operational Semantic Model for Basic SDL. Technical Report TFL RR 1991-2, Tele Danmark Research, 1991."},{"key":"19_CR26","unstructured":"H. Garavel and J. Sifakis. Compilation and Verification of LOTOS Specifications. In Proceedings of the 10th PSTV, Ottawa, Canada, June 1990."},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. Information and Computation, 111(2), 1994.","DOI":"10.1006\/inco.1994.1045"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall International, 1984.","DOI":"10.1007\/978-3-662-09507-2_19"},{"key":"19_CR29","unstructured":"Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall Software Series, 1991."},{"key":"19_CR30","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Technical Report 8807, International Organization for Standardization \u2014 Information Processing Systems \u2014 Open Systems Interconnection, 1988."},{"key":"19_CR31","unstructured":"ITU-T. Recommendation Z-100. Specification and Description Language (SDL) and Annexes F.2: Static Semantics and F.3: Dynamic Semantics. 1994."},{"key":"19_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TACAS\u201997, Enschede, The Netherlands","author":"J.P. Krimm","year":"1997","unstructured":"J.P. Krimm and L. Mounier. Compositional State Space Generation from LOTOS Programs. In Proceedings of TACAS\u201997, Enschede, The Netherlands, volume 1217 of LNCS, 1997."},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the Propositional \u00b5-Calculus. In Theoretical Computer Science. North-Holland, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"19_CR34","unstructured":"G. Le Lann. Distributed Systems-Towards a Formal Approach. In Information Processing 77. IFIP, North Holland, 1977."},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"L. Leonard and G. Leduc. An Introduction to ET-LOTOS for the Description of Time-Sensitive Systems. Computer Networks and ISDN Systems, (29), 1997.","DOI":"10.1016\/S0169-7552(96)00078-5"},{"key":"19_CR36","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u201997, Haifa, Israel","author":"K.G. Larsen","year":"1997","unstructured":"K.G. Larsen, P. Petterson, and W. Yi. UPPAAL: Status & Developments. In Proceedings of CAV\u201997, Haifa, Israel, volume 1254 of LNCS, 1997."},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking: an Approach to the State Explosion Problem. Kluwer Academic Publisher, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"19_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner. A Calculus of Communication Systems. In LNCS, number 92. 1980."},{"key":"19_CR39","unstructured":"A. Olsen, O. F\u00e6rgemand, B. M\u2205ller-Pederson, R. Reed, and J.R.W. Smith. Systems Engineering Using SDL-92. North-Holland, 1994. ISBN 0444 898727."},{"key":"19_CR40","series-title":"Technical report","volume-title":"A Tutorial on Specification and Verification Using PVS","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J.M. Rushby. A Tutorial on Specification and Verification Using PVS. Technical report, Computer Science Laboratory, SRI International, February 1993."},{"key":"19_CR41","unstructured":"J. Quemada. Final Comitee Draft on Enhancements to LOTOS. Technical report, ISO\/IEC JTC1\/SC33\/WG9, April 1998."},{"key":"19_CR42","series-title":"PhD thesis","volume-title":"Contribution at the Definition and Implementation of E-LOTOS","author":"M. Sighireanu","year":"1999","unstructured":"M. Sighireanu. Contribution at the Definition and Implementation of E-LOTOS. PhD thesis, Universit\u00e9 Joseph Fourier, Grenoble, 1999."},{"key":"19_CR43","series-title":"Lect Notes Comput Sci","volume-title":"Application and Theory of Petri Nets","author":"A. Valmari","year":"1996","unstructured":"A. Valmari. Compositionality in State Space Verification. In Application and Theory of Petri Nets, volume 1091 of LNCS, 1996."},{"key":"19_CR44","unstructured":"Verilog. ObjectGEODE SDL Simulator-Reference Manual. http:\/\/www.verilogusa.com\/solution\/pages\/ogeode.html , 1996."},{"key":"19_CR45","unstructured":"R.J. van Glabbeek and W.P. Weijland. Branching-Time and Abstraction in Bisimulation Semantics. CS R8911, CWI, 1989."},{"key":"19_CR46","doi-asserted-by":"crossref","unstructured":"S. Yovine. Kronos: A Verification Tool for Real-Time Systems. STTT, 1(1-2), Dec 1997.","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48119-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T13:27:27Z","timestamp":1556803647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48119-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665878","9783540481195"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/3-540-48119-2_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}