{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:45:19Z","timestamp":1725633919882},"publisher-location":"London","reference-count":24,"publisher":"Springer London","isbn-type":[{"type":"print","value":"9781852331078"},{"type":"electronic","value":"9781447108511"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/978-1-4471-0851-1_21","type":"book-chapter","created":{"date-parts":[[2011,11,16]],"date-time":"2011-11-16T12:27:59Z","timestamp":1321446479000},"page":"395-414","source":"Crossref","is-referenced-by-count":4,"title":["Requirements for a Temporal B Assigning Temporal Meaning to Abstract Machines\u2026 and to Abstract Systems"],"prefix":"10.1007","author":[{"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B book - Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"J.-R. Abrial. The B book - Assigning Programs to Meanings. Cambridge University Press, 1996."},{"key":"21_CR2","first-page":"169","volume-title":"1st Conference on the B method","author":"J-R Abrial","year":"1996","unstructured":"J.-R. Abrial. Extending b without changing it (for developing distributed systems). In H. Habrias, editor, 1\n                \n                  st\n                \n                Conference on the B method, pages 169\u2013190, November 1996."},{"key":"21_CR3","volume-title":"Cryptographic protocol specification and design","author":"JR Abrial","year":"1997","unstructured":"J.R. Abrial. Cryptographic protocol specification and design. Steria Meeting on protocols, May 1997."},{"key":"21_CR4","volume-title":"A problem to be studied in tla and in b (b solution)","author":"JR Abrial","year":"1997","unstructured":"J.R. Abrial and L. Mussat. A problem to be studied in tla and in b (b solution). Private Meeting on B and TLA, September 1997."},{"key":"21_CR5","volume-title":"Specification and design of a transmission protocol by sucessive refinements using B","author":"JR Abrial","year":"1997","unstructured":"J.R. Abrial and L. Mussat. Specification and design of a transmission protocol by sucessive refinements using B. Steria Meeting on Protocols, May 1997."},{"key":"21_CR6","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0167-6423(83)90004-7","volume":"3","author":"KR Apt","year":"1983","unstructured":"K. R. Apt and E. R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65\u2013100, 1983.","journal-title":"Science of Computer Programming"},{"key":"21_CR7","volume-title":"Semantics orderings and recursion in the weakest precondition calculus","author":"M Bonsangue","year":"1992","unstructured":"M. Bonsangue and J. N. Kok. Semantics, orderings and recursion in the weakest precondition calculus. Technical report, CWI, 1992."},{"key":"21_CR8","volume-title":"FME93: Industrial-Strength Formal Methods","author":"N Brown","year":"1993","unstructured":"N. Brown and D. M\u00e9ry. A Proof Environment for Concurrent Programs. In J. C. P Woodcock and P. G. Larsen, editors, FME93: Industrial-Strength Formal Methods. Springer Verlag, 1993. Lecture Notes in Computer Science 670."},{"issue":"2","key":"21_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. Transactions On Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"Transactions On Programming Languages and Systems"},{"key":"21_CR10","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF01212304","volume":"4","author":"J Fiadeiro","year":"1992","unstructured":"J. Fiadeiro and T. Maibaum. Temporal theories as modularisation units for concurrent system specification. Formal Aspects of Computing, 4:239\u2013272, 1992.","journal-title":"Formal Aspects of Computing"},{"key":"21_CR11","volume-title":"1st Irish Workshop on Formal Methods","author":"J-P Gibson","year":"1997","unstructured":"J.-P. Gibson, B. Mermet, and D. M\u00e9ry, Feature interactions: A mixed semantic model approach. In Gerard O\u2019Regan and Sharon Flynn, editors, 1st Irish Workshop on Formal Methods, Dublin, Ireland, July 1997. Irish Formal Methods Special Interest Group (IFMSIG), Springer Verlag.\n                  http:\/\/ewic.springer.co.uk\/\n                  \n                ."},{"key":"21_CR12","volume-title":"COTSR Proceedings, chapter Fair Objects, page ?? Computer Science and Electronic Engineering","author":"J-P Gibson","year":"1998","unstructured":"J.-P. Gibson and D. M\u00e9ry. COTSR Proceedings, chapter Fair Objects, page ?? Computer Science and Electronic Engineering. Horwood Publishing Ltd, October 1998."},{"issue":"3","key":"21_CR13","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"Transactions On Programming Languages and Systems"},{"key":"21_CR14","volume-title":"3rd Theory and formal Methods Workshop","author":"K Lano","year":"1996","unstructured":"K. Lano, J. Fiadeiro, and J. Dick. Extending B AMN with concurrency. In Oxford, editor, 3rd Theory and formal Methods Workshop, 1996."},{"key":"21_CR15","volume-title":"SAFECOMP97 The 16th International Conference on Computer Safety, Reliability and Security","author":"B Mermet","year":"1997","unstructured":"B. Mermet and D. M\u00e9ry. Safe combinations of services using b. In John McDermid, editor, SAFECOMP97 The 16th International Conference on Computer Safety, Reliability and Security, York, September 1997. Springer Verlag."},{"key":"21_CR16","volume-title":"Mathematical Foundations of Computer Science","author":"D M\u00e9ry","year":"1986","unstructured":"D. M\u00e9ry. A proof system to derive eventuality properties under justice hypothesis. In J. Gruszka, editor, Mathematical Foundations of Computer Science, volume 233 of Lecture Notes in Computer Science, Bratislava, august 1986. Springer Verlag."},{"issue":"3","key":"21_CR17","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1051\/ita\/1987210302871","volume":"21","author":"D M\u00e9ry","year":"1987","unstructured":"D. M\u00e9ry. M\u00e9thode axiomatique pour les propri\u00e9t\u00e9s de fatalit\u00e9 des programmes parall\u00e8les. RAIRO Informatique Th\u00e9orique et Application, 21(3):287\u2013322, 1987.","journal-title":"RAIRO Informatique Th\u00e9orique et Application"},{"key":"21_CR18","volume-title":"Computer-Aided Verification Proceedings","author":"D M\u00e9ry","year":"1992","unstructured":"D. M\u00e9ry and A. Mokkedem. Crocos: An integrated environment for interactive verification of sdl specifications. In G. Bochmann, editor, Computer-Aided Verification Proceedings, Lecture Notes in Computer Science. Springer Verlag, 1992."},{"key":"21_CR19","volume-title":"9th Symposium On Information Control in Manufacturing","author":"D M\u00e9ry","year":"1998","unstructured":"D. M\u00e9ry and J.-F. P\u00e9tin. Formal engineering methods for modelling and verification of control systems. In G. Morel and F. Vernadat, editors, 9th Symposium On Information Control in Manufacturing IN COM\u20199 8, June 24\u201326 1998."},{"issue":"3","key":"21_CR20","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. Transactions On Programming Languages and Systems, 4(3):455- 495, July 1982.","journal-title":"Transactions On Programming Languages and Systems"},{"key":"21_CR21","first-page":"259","volume-title":"Proceedings of the IBM conference","author":"D Park","year":"1981","unstructured":"D. Park. A predicate transformer for weak fair iteration. In IBM, editor, Proceedings of the IBM conference, pages 259\u2013275. IBM, IBM, 1981."},{"key":"21_CR22","first-page":"46","volume-title":"The temporal logics of programs","author":"A Pnueli","year":"1977","unstructured":"A. Pnueli. The temporal logics of programs. In Proceedings of 18th IEEE Symposium on Foundations of Computer Science, pages 46 \u2013 57, Providence, 1977. IEEE."},{"key":"21_CR23","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01898402","volume":"3","author":"BA Sanders","year":"1991","unstructured":"B. A. Sanders. Eliminating the substitution axiom from unity logic. Formal Aspects of Computing, 3:189\u2013205, 1991.","journal-title":"Formal Aspects of Computing"},{"key":"21_CR24","unstructured":"Steria M\u00e9diterrann\u00e9e.Atelier B, Version 3.2, Manuel de R\u00e9f\u00e9rence du Langage B. GEC Alsthom Transport and Steria M\u00e9diterrann\u00e9e and SNCF and INRETS and RATP, 1997."}],"container-title":["IFM\u201999"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-0851-1_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,1]],"date-time":"2021-05-01T00:50:38Z","timestamp":1619830238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-0851-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9781852331078","9781447108511"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-0851-1_21","relation":{},"subject":[],"published":{"date-parts":[[1999]]}}}