Abstract
This paper proposes a development process for interactive systems based both on verification and validation methods. Our approach is formal and use at first the B Method. We show in this paper how formal B specifications can be derived from informal requirements in the informal notation UAN. Then, these B specifications are validated using the data oriented specification language EXPRESS. Several scenarios can be tested against these EXPRESS specifications.
Chapter PDF
Similar content being viewed by others
Key words
References
Abrial, J.-R. (1996) The B Book: Assigning Programs to Meanings. Cambridge University Press.
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’96) (5–7 June, Namur, Belgium), Springer-Verlag, pp. 92–104.
Ahlberg, C. and Truve, S. (1995) Tight Coupling: Guiding User Actions in a Direct Manipulation Retrieval System. In Proceedings of HCI’95 Conference on People and Computers X, pp. 305–321.
Aït-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’98) (3–5 June, Abingdon, UK), pp. 333–352.
Aït-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–108.
Bouazza, M. (1995) Le langage EXPRESS. Hermès, Paris.
Brun, P. (1997) XTL: a temporal logic for the formal development of interactive systems. Palanque, P. et Paternò, F. (Ed.). In Formal Methods for Human-Computer Interaction, Springer-Verlag, pp. 121–139.
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–263.
ClearSy. (1997) Atelier B-version 3.5. 1997.
Dijkstra, E. (1976) A Discipline of Programming. Prentice Hall, Englewood Cliff (NJ), USA.
EXPRESS. (1994) The EXPRESS language reference manual. ISO, 1994 ISO 10303-11.
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–5, Zurich, Switzerland).
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.
Guittet, L. (1995) Contribution à l’Ingénierie des Interfaces Homme-Machine-Théorie des Interacteurs et Architecture H4 dans le système NODAOO. Doctorat d’Université (PhD Thesis): Université de Poitiers.
Hix, D. and Hartson, H.R. (1993) Developping user interfaces: Ensuring usability through product & process. John Wiley & Sons, inc., Newyork, USA.
Hoare, C.A.R. (1969) An Axiomatic Basis for Computer Programming. CACM. 12, 10, pp. 576–583.
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.
Jambon, F. (2002) From Formal Specifications to Secure Implementations. In Proceedings of Computer-Aided Design of User Interfaces (CADUI’2002) (May 15–17, Valenciennes, France), Kluwer Academics, pp. 43–54.
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’99) (2–4 June, Universidade do Minho, Braga, Portugal), Springer-Verlag, pp. 205–224.
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–60.
Marshall, L.S. (1986) A Formal Description Method for User Interface. Ph.D Thesis: University of Manchester.
McMillian, K. (1992) The SMV System. Carnegie Mellon University, 1992.
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’2000 (Limerick, Ireland), Springer Verlag.
Paternò, F. and Faconti, G.P. (1992) On the LOTOS use to describe graphical interaction. In Cambridge University Press, pp. 155–173.
Paternò, 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’95) (14–18 August, Grand Targhee Resort (Yellowstone Park), USA), Chapman & Hall, 1995, pp. 213–226.
Roché, P. (1998) Modélisation et validation d’interface homme-machine. Doctorat d’Université (PhD Thesis): École Nationale Supérieure de l’Aéronautique et de l’Espace.
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–380.
Schenck, D. and Wilson, P. (1994) Information Modelling The EXPRESS Way. Oxford University Press.
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–55.
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–393.
Wellner, P. (1989) StateMaster: a UIMS based on Statecharts for prototyping and target implementation. In Proceedings of Human Factors in Computing Systems (CHI’89) (30 April–4 May, Austin, USA), ACM/SIGCHI, pp. 177–182.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science + Business Media, Inc.
About this paper
Cite this paper
Aït-Ameur, Y., Breholée, B., Girard, P., Guittet, L., Jambon, F. (2004). Formal Verification and Validation of Interactive Systems Specifications. In: Johnson, C.W., Palanque, P. (eds) Human Error, Safety and Systems Development. IFIP International Federation for Information Processing, vol 152. Springer, Boston, MA. https://doi.org/10.1007/1-4020-8153-7_5
Download citation
DOI: https://doi.org/10.1007/1-4020-8153-7_5
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4020-8152-1
Online ISBN: 978-1-4020-8153-8
eBook Packages: Springer Book Archive