Abstract
This paper proposes a new tool-supported technique for the complete development of safety-critical interactive systems from the specification to the implementation step. Safety as well as usability properties are continuously guaranteed during the development process. This technique relies on formal specifications of the requirements and so uses the model-oriented formal method B and a new ad-hoc software architecture model -CAV- which is an hybrid of MVC and PAC models. At the implementation step, this technique uses automatic code generation. Moreover, links from secure generated code to native non-secure libraries are clarified. This development process is illustrated by a fully implemented case study.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R., The B Book: Assigning Programs to Meanings, Cambridge University Press, Cambridge, 1996.
Aït-Ameur, Y., Girard, P., and Jambon, F., Using the B formal approachfor incremental specification design of Interactive Systems, in S. Chatty and P. Dewan (eds.), Engineering for Human-Computer Interaction, Vol. 22, Kluwer Academic Publishers, Dordrecht, 1998, pp. 91–108.
Bass, L., Pellegrino, R., Reed, S., Sheppard, S., and Szczur, M., A Metamodel for the Runtime Architecture of an Interactive System, The UIMS Workshop Tool Developers, SIGCHI Bulletin, Vol. 24, No. 1, 1992, pp. 32–37.
Brun, P., XTL: a temporal logic for the formal development of Interactive Systems, in P. Palanque and F. Paternò (eds.), Formal Methods for Human-Computer Interaction, Springer-Verlag, 1997, pp. 121–139.
ClearSy. Atelier B - version 3.5, 1997.
Jambon, F., Girard, P., and Aït-Ameur, Y., Interactive System Safety and Usability enforced with the development process, in Proc. Engineering for Human-Computer Interaction EHCI’01 (Toronto, May 11–13, 2001), PREceedings, 2001, pp. 61–76.
Duke, DJ. and Harrison, M.D., Abstract Interaction Objects, Computer Graphics Forum, Vol. 12, No. 3, 1993, pp. 25–36.
Paternò, F., A Theory of User-Interaction Objects, Journal of Visual Languages and Computing, Vol. 5, No. 3, 1994, pp. 227–249.
Paternò, F. and Faconti, G.P., On the LOTOS use to describe graphical interaction, Proc. of HCI’92 Conf, Cambridge University Press, Cambridge, 1992, pp. 155–173.
Palanque, P., Modélisation par Objets Coopératifs Interactifs d’interfaces homme-machine dirigées par Vutilisateur, Ph.D. thesis, Université de Toulouse I, Toulouse, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Jambon, F. (2002). From Formal Specifications to Secure Implementations. In: Kolski, C., Vanderdonckt, J. (eds) Computer-Aided Design of User Interfaces III. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-0421-3_4
Download citation
DOI: https://doi.org/10.1007/978-94-010-0421-3_4
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-3915-4
Online ISBN: 978-94-010-0421-3
eBook Packages: Springer Book Archive