{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:33:14Z","timestamp":1725489194346},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417910"},{"type":"electronic","value":"9783540452515"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45251-6_21","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T01:53:28Z","timestamp":1186883608000},"page":"384-395","source":"Crossref","is-referenced-by-count":6,"title":["An Adequate Logic for Full LOTOS"],"prefix":"10.1007","author":[{"given":"Muffy","family":"Calder","sequence":"first","affiliation":[]},{"given":"Savi","family":"Maharaj","sequence":"additional","affiliation":[]},{"given":"Carron","family":"Shankland","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,16]]},"reference":[{"key":"21_CR1","unstructured":"D. Amyot, L. Char et al. Feature Description and Feature Interaction Analysis with Use Case Maps and LOTOS. In M. Calder and E. Magill, editors, Feature Interactions in Telecommunications and Software Systems VI. IOS Press, May 2000."},{"key":"21_CR2","unstructured":"H. Becht, A. Bloesch et al. Ergo 4.1 Reference Manual. Technical Report 96-31, Software Verification Research Centre, University of Queensland, Australia, November 1996"},{"key":"21_CR3","unstructured":"M. Calder, S. Maharaj, and C. Shankland. A Modal Logic for Early Symbolic Transition Systems. The Computer Journal, 2001. To appear."},{"key":"21_CR4","unstructured":"M. Calder and C. Shankland. A Symbolic Semantics and Bisimulation for Full LOTOS. To appear as a University of Stirling Technical Report, 2000."},{"key":"21_CR5","unstructured":"M. Clavel, F. Duran et al. Maude: Specification and Programming in Rewriting Logic. Maude System documentation. Computer Science Laboratory, SRI, Menlo Park, California, March 1999."},{"key":"21_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"CADP (CAESAR\/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox","author":"J.-C. Fernandez","year":"1996","unstructured":"J-C. Fernandez, H. Garavel et al. CADP (CAESAR\/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In R. Alur and T.A. Henzinger, editors, Proceedings of CAV\u201996, number 1102 in Lecture Notes in Computer Science, pages 437\u2013440. Springer-Verlag, 1996."},{"key":"21_CR7","series-title":"Lect Notes Comput Sci","first-page":"74","volume-title":"Verification of Temporal Properties of Processes in a Setting with Data","author":"J.F. Groote","year":"1999","unstructured":"J.F. Groote and R. Mateescu. Verification of Temporal Properties of Processes in a Setting with Data. In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology AMAST\u201998, Amazonia, Brazil, volume 1548 of Lecture Notes in Computer Science, pages 74\u201390, 1999."},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"J.F. Groote and A. Ponse. The Syntax and Semantics of \u00b5-CRL. In Proceedings of Algebra of Communicating Processes, Utrecht 1994, Workshops in Computing. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"M. Hennessy and H. Lin. Symbolic Bisimulations. Theoretical Computer Science, 138:353\u2013389, 1995.","DOI":"10.1016\/0304-3975(94)00172-F"},{"key":"21_CR10","first-page":"375","volume":"32","author":"M. Hennessy","year":"1995","unstructured":"M. Hennessy and X. Liu. A Modal Logic for Message Passing Processes. Acta Informatica, 32:375\u2013393, 1995.","journal-title":"A Modal Logic for Message Passing Processes"},{"issue":"1","key":"21_CR11","first-page":"137","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery, 32(1):137\u2013161, 1985.","journal-title":"Algebraic Laws for Nondeterminism and Concurrency"},{"key":"21_CR12","unstructured":"International Organisation for Standardisation. Information Processing Systems\u2013Open Systems Interconnection\u2013LOTOS\u2013A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, 1988."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"C. Kirkwood. Specifying Properties of Basic LOTOS Processes Using Temporal Logic. In G. v Bochmann, R. Dssouli, and O. Rafiq, editors, Formal Description Techniques, VIII, IFIP. Chapman Hall, April 1996.","DOI":"10.1007\/978-0-387-34945-9_8"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the Propositional \u00b5-Calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"21_CR15","unstructured":"R. Mateescu and H. Garavel. XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. In Proceedings of the International Workshop on Software Tools for Technology Transfer STTT\u201998 (Aalborg, Denmark), 1998."},{"issue":"2","key":"21_CR16","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0140-3664(92)90129-3","volume":"15","author":"C. Pecheur","year":"1992","unstructured":"C. Pecheur. Using LOTOS for specifying the CHORUS distributed operating system kernel. Computer Communications, 15(2):93\u2013102, March 1992.","journal-title":"Computer Communications"},{"issue":"1","key":"21_CR17","first-page":"68","volume":"2","author":"M. Sighireanu","year":"1998","unstructured":"M. Sighireanu and R. Mateescu.Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): an Experiment with E-LOTOS. Springer International Journal on Software Tools for Technology Transfer (STTT), 2(1):68\u201388, Dec. 1998.","journal-title":"Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): an Experiment with E-LOTOS"},{"key":"21_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/BFb0013039","volume-title":"Temporal Logics for CCS","author":"C. Stirling","year":"1989","unstructured":"C. Stirling. Temporal Logics for CCS. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, pages 660\u2013672. Springer-Verlag, 1989. REX School \/Workshop, Noordwijkerhout, The Netherlands, May\/June 1988."},{"issue":"1","key":"21_CR19","first-page":"3","volume":"1","author":"M. Thomas","year":"1994","unstructured":"M. Thomas. The Story of the Therac-25 in LOTOS. High Integrity Systems Journal, 1(1):3\u201315, 1994.","journal-title":"The Story of the Therac-25 in LOTOS"},{"key":"21_CR20","unstructured":"M. Thomas. Modelling and Analysing User Views of Telecommunications Services. In Feature Interactions in Telecommunications Systems, pages 168\u2013183. IOS Press, 1997."},{"issue":"1","key":"21_CR21","first-page":"15","volume":"2","author":"M. Thomas","year":"1994","unstructured":"M. Thomas and B. Ormsby. On the Design of Side-Stick Controllers in Fly-by-Wire Aircraft. A.C.M. Applied Computing Review, 2(1):15\u201320, Spring 1994.","journal-title":"On the Design of Side-Stick Controllers in Fly-by-Wire Aircraft"},{"issue":"15","key":"21_CR22","first-page":"1389","volume":"30","author":"K. J. Turner","year":"1998","unstructured":"Kenneth J. Turner. An architectural description of intelligent network features and their interactions. Computer Networks, 30(15):1389\u20131419, September 1998.","journal-title":"Computer Networks"},{"key":"21_CR23","unstructured":"A. Vogel. On ODP\u2019s architectural semantics using LOTOS. In J. de Meer, B. Mahr, and O. Spaniol, editors, Proc. Int. Conf. on Open Distributed Processing, pages 340\u2013345, September 1993."}],"container-title":["Lecture Notes in Computer Science","FME 2001: Formal Methods for Increasing Software Productivity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45251-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:48:36Z","timestamp":1556740116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45251-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417910","9783540452515"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45251-6_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}