{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T18:40:45Z","timestamp":1771008045599,"version":"3.50.1"},"publisher-location":"Vienna","reference-count":19,"publisher":"Springer Vienna","isbn-type":[{"value":"9783211832127","type":"print"},{"value":"9783709136935","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/978-3-7091-3693-5_16","type":"book-chapter","created":{"date-parts":[[2013,7,4]],"date-time":"2013-07-04T10:43:00Z","timestamp":1372934580000},"page":"242-260","source":"Crossref","is-referenced-by-count":11,"title":["Using Model Checking for the Automatic Validation of User Interfaces Systems"],"prefix":"10.1007","author":[{"given":"Bruno","family":"d\u2019Ausbourg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","first-page":"44","volume-title":"Integrating status and event phenomena in formal specifications of interactive systems","author":"GD Abowd","year":"1994","unstructured":"G.D. Abowd and A.J. Dix. Integrating status and event phenomena in formal specifications of interactive systems. SIGSOFT\u201994, ACM Press, pp. 44\u201352, 1994."},{"key":"16_CR2","volume-title":"Proceddings of the First Symposium on Designing Interactive Systems, DIS\u201995,Ann","author":"GD Abowd","year":"1995","unstructured":"G.D. Abowd, H.M. Wang and A.F. Monk. A formal technique for automated dialogue development. In Proceddings of the First Symposium on Designing Interactive Systems, DIS\u201995,Ann Arbor, MI, ACM Press, August 1995."},{"key":"16_CR3","volume-title":"Proceedings of DSVIS96","author":"B d\u2019Ausbourg","year":"1996","unstructured":"B. d\u2019Ausbourg, G. Durrieu and P. Roche. Deriving a formal model of an interactive system from its UIL description in order to verify and to test its behaviour. In Proceedings of DSVIS96, Namur, Belgium, June 1996."},{"key":"16_CR4","volume-title":"Proceedings of the 20th International Conference on Software Engineering (ICSE\u201998)","author":"B d\u2019Ausbourg","year":"1998","unstructured":"B. d\u2019Ausbourg, C. Seguin, G. Durrieu and P. Roche. Assisting the Automated Validation Process of User Interface Systems In Proceedings of the 20th International Conference on Software Engineering (ICSE\u201998), Kyoto, Japan, 1998."},{"key":"16_CR5","volume-title":"14th ACM Symposium on Principles of Programming Languages","author":"P Caspi","year":"1987","unstructured":"P. Caspi, D. Pilaud, N. Halbwachs and J. Plaice. Lustre: a declarative language for programming synchronous systems, in 14th ACM Symposium on Principles of Programming Languages, January 1987."},{"key":"16_CR6","volume-title":"Proceedings of SIGSOFT\u201988. Third Annual Symposium on Software Development Environments (SDE3), Boston","author":"D Clement","year":"1988","unstructured":"D. Clement, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang and V. Pascual. Centaur: the system. In Proceedings of SIGSOFT\u201988. Third Annual Symposium on Software Development Environments (SDE3), Boston, 1988."},{"key":"16_CR7","volume-title":"Formal methods for interactive systems","author":"AJ Dix","year":"1991","unstructured":"A.J. Dix. Formal methods for interactive systems. Academic Press, 1991."},{"key":"16_CR8","volume-title":"Software Engineering journal","author":"AJ Dix","year":"1996","unstructured":"A.J. Dix and G.D. Abowd. Modelling status and event behaviour of interactive systems. In Software Engineering journal, November 1996."},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1111\/1467-8659.1230025","volume":"12","author":"DJ Duke","year":"1993","unstructured":"D.J. Duke and M.D. Harrison. Abstract interaction objetcs. Computer Graphics Forum,1993, 12, n\u00b03, pp. 25\u201326.","journal-title":"Computer Graphics Forum"},{"key":"16_CR10","volume-title":"Software Engineering journal","author":"DJ Duke","year":"1995","unstructured":"D.J. Duke and M.D. Harrison. Event model of human system interaction. In Software Engineering journal, January 1995."},{"key":"16_CR11","volume-title":"Proceedings of Advance Visual Interface\u2019 94 Workshop","author":"DJ Duke","year":"1994","unstructured":"D.J. Duke, G. Faconti, M.D. Harrison and F. Paterno. Unifying views of interactors. In Proceedings of Advance Visual Interface\u2019 94 Workshop, Bari, 1994"},{"key":"16_CR12","volume-title":"Proceedings of the ICSE\u201994 Workshop","author":"MD Harrison","year":"1994","unstructured":"M.D. Harrison and D.J. Duke. A review of formalisms for describing interactive behaviour. In Proceedings of the ICSE\u201994 Workshop, R.N Taylor and J. Coutaz, editors, Software Engineering and Human Computer Interaction, LNCS806, May 1994."},{"key":"16_CR13","volume-title":"Eurographics90","author":"G Faconti","year":"1990","unstructured":"G. Faconti and F. Paterno. An approach to the formal specification of the components of an interaction. In Eurographics90, 1990."},{"key":"16_CR14","first-page":"1305","volume-title":"Proceedings of IEEE","author":"N Halbwachs","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud. The synchronous dataflow programming language Lustre. In Proceedings of IEEE, number 9 in 79, pp. 1305\u20131320, September 1991."},{"key":"16_CR15","first-page":"795","volume-title":"Programming and verifying Real Time Systems by Means of the Synchronous DataFlow Programming Language Lustre","author":"N Halbwachs","year":"1992","unstructured":"N. Halbwachs, F. Lagnier and C. Ratel. Programming and verifying Real Time Systems by Means of the Synchronous DataFlow Programming Language Lustre. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real Time Systems, pp 795\u2013793, Spetember 1992."},{"key":"16_CR16","volume-title":"Motif Programming Manual","author":"D Heller","year":"1994","unstructured":"D. Heller, P. Ferguson and D. Brerinan. Motif Programming Manual. O\u2019Reilly and Associates Inc, February 1994."},{"key":"16_CR17","volume-title":"People and Computers VII; HCI\u201992 Conference","author":"F Paterno","year":"1992","unstructured":"F. Paterno and G. Faconti. On the use of Lotos to describe graphical interaction. In A. Monk, D.Diaper, and M.D. Harrison, editors, People and Computers VII; HCI\u201992 Conference, BCS HCI Specialist Group, Cambridge University Press, 1992."},{"key":"16_CR18","volume-title":"Proceeedings EH CI\u201995 Conference","author":"F Paterno","year":"1995","unstructured":"F. Paterno and M. Mezzanotte. Formal verification of undesired behaviours in the CERD case study. In Proceeedings EH CI\u201995 Conference, Wyoming, August 1995."},{"key":"16_CR19","volume-title":"Symposium on Formal Techniques in Real Time and Fault Tolerant Systems","author":"D Pilaud","year":"1998","unstructured":"D. Pilaud and N. Halbwachs. From a synchronous delarative language to a temporal logic dealing with multiform time. In Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Springer Verlag, September 1988."}],"container-title":["Eurographics","Design, Specification and Verification of Interactive Systems \u201998"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-7091-3693-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T07:31:47Z","timestamp":1557905507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-7091-3693-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783211832127","9783709136935"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-7091-3693-5_16","relation":{},"ISSN":["0946-2767"],"issn-type":[{"value":"0946-2767","type":"print"}],"subject":[],"published":{"date-parts":[[1998]]}}}