Abstract
This chapter describes the work of AeS in the context of the DEPLOY Associate program. It outlines the progress of the pilot project, the development of a specification of a simple railway system called “dead man control”. In addition to this, we also present some parallel developments, some of them theoretical and others practical, in the use of formal methods in industry, focusing on such important points as requirements validation, productivity and dependability.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Beck, K.: Test Driven Development: By Example. Addison-Wesley Longman Publishing, Boston (2002)
Butler, M., Hallerstede, S.: The Rodin formal modelling tool. http://deploy-eprints.ecs.soton.ac.uk/4/1/eventb.pdf
Darimont, R., van Lamsweerde, A.: Formal refinement patterns for goal-driven requirements elaboration. In: Proceedings of the 4th ACM SIGSOFT Symposium on Foundations of Software Engineering (1996)
Gunter, C., Gunter, E., Jackson, M., Zave, P.: A reference model for requirements and specifications. IEEE Softw. 41 (2000)
Jackson, M.: Problem Frames: Analyzing and Structuring Software Development Problems. Addison-Wesley Longman Publishing, Boston (2001)
Jacobson, I.: Object-oriented development in an industrial environment. In: OOPSLA ’87: Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications, pp. 183–191. ACM, New York (1987)
Jacobson, I.: Object-Oriented Software Engineering: A Use Case Driven Approach. Addison-Wesley, Reading (1992)
Jastram, M., Leuschel, M., Bendisposto, J.: Mapping requirements to B models. DEPLOY Deliverable. Unpublished manuscript (2009)
Ledang, H.: Automatic translation from UML specifications to B. In: Proceedings of the 16th Annual International Conference on Automated Software Engineering Conference—ASE 2001. IEEE Comput. Soc., Los Alamitos (2001)
Ochodek, M., Nawrocki, J.: Automatic transactions identification in use cases. In: The 2nd IFIP TC-2 Central and East European Conference on Software Engineering Techniques, CEE-SET 2007, Poznan, Poland, October 10–12, 2007, Revised Selected, pp. 55–68. Springer, Berlin (2008)
Ponsard, C., Dieul, E.: From requirements models to formal specifications in B. In: ReMo2V CEUR Workshop Proceedings, vol. 241 (2006)
ProB: Animator and model checker. http://www.stups.uni-duesseldorf.de/ProB (February 2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Russo, A.G. (2013). Formal Methods as an Improvement Tool. In: Romanovsky, A., Thomas, M. (eds) Industrial Deployment of System Engineering Methods. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33170-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-33170-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33169-5
Online ISBN: 978-3-642-33170-1
eBook Packages: Computer ScienceComputer Science (R0)