Abstract
Our goal in this paper is not to enrich the literature with yet another defence of formal methods, but rather to build on our experience of using and studying formal methods in security to provide an industrial point of view, with a strong emphasis on practicality. We also hope that, even if we take our inspiration mainly in the security area, most of our observations on formal methods are relevant to other application domains as well. The term “security”itself can be used in various contexts with different meanings. We use it here in the sense of security of information, as defined by the standard triptych: confidentiality, integrity and availability.
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.
References
Abrial, J. R.: “Assigning programs to meaning”. Cambridge University Press 1996.
Bochmann, G., Petrenko, A.: “Protocol testing: review of methods and relevance for software testing”. Proc. of the ACM int. Symposium on software testing and analysis 1994.
Booch, G., Rumbaugh, J., Jacobson, I.: “The Unified Modeling Language user guide”. Addison-Wesley 1998.
Bowman, H., Boiten, E., Derrick, J., Steen, M.: “Viewpoint consistency in ODP, a general interpretation”. Proc. of the 1st IFIP int. Workshop on formal methods for open object-based distributed systems, Chapman & Hall 1996, pp. 189–204.
“The Common Criteria for Information Technology Security Evaluation”. http://www.commoncriteria.org/docs/aboutus.html.
De Millo, R. A., Lipton, R. J., Perlis, A. J.: “Social processes and proofs of theorems and programs”. Communications of the ACM, 22(5) 1979, pp. 271–280.
Fernandez, J-C., Jard, C., Jéron, T., Viho, C.: “An experiment in automatic generation of test suites for protocols with verification technology”. Science of Computer Programming, Vol. 28, 1997, pp. 123–146.
Fradet, P., Le Métayer, D., Périn, M.: “Consistency checking for multiple view software architecture”. Proc. 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Springer Verlag, LNCS 1687, 1999, pp. 410–428.
Kruchten, P-B.: “The 4+1 view model of architecture”. IEEE Software, 12(6), 1995, pp. 42–50.
“The Precise UML (PUML) group”http://www.cs.york.ac.uk/puml/.
Spivey, J.: “The Z reference manual”. Prentice Hall, 1992.
Van Aertryck, L., Benveniste, M., Le Métayer, D.: “Casting: a formally based software test generation method”. IEEE int. Conference on formal engineering methods, 1997, pp. 101–111.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bolignano, D., Le Métayer, D., Loiseaux, C. (2001). Formal Methods in Practice: The Missing Links. A Perspective from the Security Area. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds) Modeling and Verification of Parallel Processes. MOVEP 2000. Lecture Notes in Computer Science, vol 2067. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45510-8_7
Download citation
DOI: https://doi.org/10.1007/3-540-45510-8_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42787-2
Online ISBN: 978-3-540-45510-3
eBook Packages: Springer Book Archive