{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:26:16Z","timestamp":1725459976941},"publisher-location":"Boston","reference-count":31,"publisher":"Kluwer Academic Publishers","isbn-type":[{"type":"print","value":"1402081529"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8153-7_5","type":"book-chapter","created":{"date-parts":[[2006,3,2]],"date-time":"2006-03-02T08:13:59Z","timestamp":1141287239000},"page":"61-76","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification and Validation of Interactive Systems Specifications"],"prefix":"10.1007","author":[{"given":"Yamine","family":"A\u00eft-Ameur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benoit","family":"Brehol\u00e9e","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Girard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Guittet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francis","family":"Jambon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R. (1996) The B Book: Assigning Programs to Meanings. Cambridge University Press.","DOI":"10.1017\/CBO9780511624162"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Accott, J., Chatty, S. and Palanque, P. (1996) A formal description of low level interaction and its application to multimodal interactive systems. In Proceedings of Eurographics Workshop on Design, Specification, and Verification of Interactive Systems (DSV-IS\u201996) (5\u20137 June, Namur, Belgium), Springer-Verlag, pp. 92\u2013104.","DOI":"10.1007\/978-3-7091-7491-3_5"},{"key":"5_CR3","unstructured":"Ahlberg, C. and Truve, S. (1995) Tight Coupling: Guiding User Actions in a Direct Manipulation Retrieval System. In Proceedings of HCI\u201995 Conference on People and Computers X, pp. 305\u2013321."},{"key":"5_CR4","unstructured":"A\u00eft-Ameur, Y., Girard, P. and Jambon, F. (1998a) A Uniform approach for the Specification and Design of Interactive Systems: the B method. In Proceedings of Eurographics Workshop on Design, Specification, and Verification of Interactive Systems (DSV-IS\u201998) (3\u20135 June, Abingdon, UK), pp. 333\u2013352."},{"key":"5_CR5","unstructured":"A\u00eft-Ameur, Y., Girard, P. and Jambon, F. (1998) Using the B formal approach for incremental specification design of interactive systems. In Proc. of Engineering for Human-Computer Interaction, Kluwer Academic Publishers, pp. 91\u2013108."},{"key":"5_CR6","volume-title":"Le langage EXPRESS","author":"M. Bouazza","year":"1995","unstructured":"Bouazza, M. (1995) Le langage EXPRESS. Herm\u00e8s, Paris."},{"key":"5_CR7","unstructured":"Brun, P. (1997) XTL: a temporal logic for the formal development of interactive systems. Palanque, P. et Patern\u00f2, F. (Ed.). In Formal Methods for Human-Computer Interaction, Springer-Verlag, pp. 121\u2013139."},{"issue":"8","key":"5_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"2","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A. and Sistla, A. P. (1986) Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems. 2, 8, pp. 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR9","unstructured":"ClearSy. (1997) Atelier B-version 3.5. 1997."},{"key":"5_CR10","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E. (1976) A Discipline of Programming. Prentice Hall, Englewood Cliff (NJ), USA."},{"key":"5_CR11","unstructured":"EXPRESS. (1994) The EXPRESS language reference manual. ISO, 1994 ISO 10303-11."},{"key":"5_CR12","unstructured":"Girard, P., Baron1, M. and Jambon, F. (2003) Integrating formal approaches in Human-Computer Interaction. In Proceedings of INTERACT 2003-Bringing the Bits togETHer-Ninth IFIP TC13 International Conference on Human-Computer Interaction-Workshop Closing the Gaps: Software Engineering and Human-Computer Interaction, (September 1\u20135, Zurich, Switzerland)."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Gray, P., England, D. and McGowan, S. (1994) XUAN: Enhancing the UAN to capture temporal relation among actions. Department of Computing Science, University of Glasgow, February, Department research report IS-94-02.","DOI":"10.1017\/CBO9780511600821.023"},{"key":"5_CR14","unstructured":"Guittet, L. (1995) Contribution \u00e0 l\u2019Ing\u00e9nierie des Interfaces Homme-Machine-Th\u00e9orie des Interacteurs et Architecture H4 dans le syst\u00e8me NODAOO. Doctorat d\u2019Universit\u00e9 (PhD Thesis): Universit\u00e9 de Poitiers."},{"key":"5_CR15","volume-title":"Developping user interfaces: Ensuring usability through product & process","author":"D. Hix","year":"1993","unstructured":"Hix, D. and Hartson, H.R. (1993) Developping user interfaces: Ensuring usability through product & process. John Wiley & Sons, inc., Newyork, USA."},{"issue":"10","key":"5_CR16","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R. (1969) An Axiomatic Basis for Computer Programming. CACM. 12, 10, pp. 576\u2013583.","journal-title":"CACM"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., Hayes, I.J., Jifeng, H., Morgan, C.C., Sanders, A.W., Sorensen, I.H., Spivey, J.M. and Sufrin, B.A. (1987) Laws of Programming. CACM. 30, 8.","DOI":"10.1145\/27651.27653"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Jambon, F. (2002) From Formal Specifications to Secure Implementations. In Proceedings of Computer-Aided Design of User Interfaces (CADUI\u20192002) (May 15\u201317, Valenciennes, France), Kluwer Academics, pp. 43\u201354.","DOI":"10.1007\/978-94-010-0421-3_4"},{"key":"5_CR19","first-page":"205","volume-title":"Dialogue Validation from Task Analysis","author":"F. Jambon","year":"1999","unstructured":"Jambon, F., Girard, P. and Boisdron, Y. (1999) Dialogue Validation from Task Analysis. In Proceedings of Eurographics Workshop on Design, Specification, and Verification of Interactive Systems (DSV-IS\u201999) (2\u20134 June, Universidade do Minho, Braga, Portugal), Springer-Verlag, pp. 205\u2013224."},{"issue":"2","key":"5_CR20","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1049\/sej.1995.0008","volume":"10","author":"C.W. Johnson","year":"1995","unstructured":"Johnson, C.W. (1995) Using Z to support the design of interactive, safety-critical systems. IEE\/BCS Software Engineering Journal. 10, 2 (March), pp. 49\u201360.","journal-title":"IEE\/BCS Software Engineering Journal"},{"key":"5_CR21","unstructured":"Marshall, L.S. (1986) A Formal Description Method for User Interface. Ph.D Thesis: University of Manchester."},{"key":"5_CR22","unstructured":"McMillian, K. (1992) The SMV System. Carnegie Mellon University, 1992."},{"key":"5_CR23","volume-title":"Structuring interactive systems specifications for executability and prototypability","author":"D. Navarre","year":"2000","unstructured":"Navarre, D., Palanque, P., Bastides, R. and Sy, O. (2000) Structuring interactive systems specifications for executability and prototypability. In Proceedings of 7th Eurographics workshop on Design, Specification and Verification of Interactive Systems, DSV-IS\u20192000 (Limerick, Ireland), Springer Verlag."},{"key":"5_CR24","unstructured":"Patern\u00f2, F. and Faconti, G.P. (1992) On the LOTOS use to describe graphical interaction. In Cambridge University Press, pp. 155\u2013173."},{"key":"5_CR25","unstructured":"Patern\u00f2, F. and Mezzanotte, M. (1995) Formal verification of undesired behaviours in the CERD case study. In Proceedings of IFIP TC2\/WG2.7 Working Conference on Engineering for Human-Computer Interaction (EHCI\u201995) (14\u201318 August, Grand Targhee Resort (Yellowstone Park), USA), Chapman & Hall, 1995, pp. 213\u2013226."},{"key":"5_CR26","unstructured":"Roch\u00e9, P. (1998) Mod\u00e9lisation et validation d\u2019interface homme-machine. Doctorat d\u2019Universit\u00e9 (PhD Thesis): \u00c9cole Nationale Sup\u00e9rieure de l\u2019A\u00e9ronautique et de l\u2019Espace."},{"key":"5_CR27","first-page":"371","volume-title":"Working with display units","author":"D.L. Scapin","year":"1990","unstructured":"Scapin, D.L. and Pierret-Golbreich, C. (1990) Towards a method for task description: MAD. Berliguet, L. et Berthelette, D. (Ed.). In Working with display units, Elsevier Science Publishers, North-Holland, pp. 371\u2013380."},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Schenck, D. and Wilson, P. (1994) Information Modelling The EXPRESS Way. Oxford University Press.","DOI":"10.1093\/oso\/9780195087147.001.0001"},{"key":"5_CR29","first-page":"15","volume-title":"Task Analysis for Human-Computer Interaction","author":"A. Shepherd","year":"1989","unstructured":"Shepherd, A. (1989) Analysis and training in information technology tasks. Diaper, D. (Ed.). In Task Analysis for Human-Computer Interaction, Ellis Horwood, Chichester, USA, pp. 15\u201355."},{"key":"5_CR30","unstructured":"Waserman, A. (1981) User Software Engineering and the design of Interactive Systems. In Proceedings of 5th IEEE International Conference on Software Engineering, IEEE society press, 1981, pp. 387\u2013393."},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Wellner, P. (1989) StateMaster: a UIMS based on Statecharts for prototyping and target implementation. In Proceedings of Human Factors in Computing Systems (CHI\u201989) (30 April\u20134 May, Austin, USA), ACM\/SIGCHI, pp. 177\u2013182.","DOI":"10.1145\/67449.67486"}],"container-title":["IFIP International Federation for Information Processing","Human Error, Safety and Systems Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8153-7_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,24]],"date-time":"2021-07-24T12:30:16Z","timestamp":1627129816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8153-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081529"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8153-7_5","relation":{},"subject":[]}}