Abstract
Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements.
We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.
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.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Abrial, J.-R.: Formal Methods in Industry: Achievements, Problems, Future. In: Proc. of the 28th Int. Conf. on Software Engineering, pp. 761–768 (2006)
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)
Berry, D.M.: Formal Methods: The Very Idea – Some Thoughts About Why They Work When They Work. Science of Computer Programming 42(1), 11–27 (2002)
Bjørner, D.: From Domain to Requirements. In: Concurrency, Graphs and Models: Essays dedicated to Ugo Montanari on the Occasion of his 65th Birthday, pp. 278–300. Springer, Heidelberg (2008)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009)
Darimont, R., Delor, E., Massonet, P., van Lamsweerde, A.: GRAIL/KAOS: An Environment for Goal-Driven Requirements Engineering. In: Proc. of the 19th Int. Conf. on Software Engineering, pp. 612–613. ACM, New York (1997)
Gotel, O., Finkelstein, A.: An Analysis of the Requirements Traceability Problem. In: Proc. of the First Int. Conf. on Requirements Engineering, pp. 94–101 (1994)
Gunter, C.A., Jackson, M., Gunter, E.L., Zave, P.: A Reference Model for Requirements and Specifications. IEEE Software 17, 37–43 (2000)
Hallerstede, S., Leuschel, M.: How to Explain Mistakes. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 105–124. Springer, Heidelberg (2009)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Jackson, M.: Problem Frames: Analysing and Structuring Software Development Problems. Addison-Wesley/ACM Press (2001)
Jastram, M.: Requirements Traceability. Technical report, U. Southampton (2009)
Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Englewood Cliffs (1990)
Leuschel, M., Butler, M.: ProB: An Automated Analysis Toolset for the B Method. Int. Journal on Software Tools for Technology Transfer 10(2), 185–203 (2008)
Loesch, F., Gmehlich, R., Grau, K., Jones, C., Mazzara, M.: Report on Pilot Deployment in Automotive Sector. Technical Report D7, DEPLOY Project (2010)
Marincic, J., Wupper, H., Mader, A.H., Wieringa, R.J.: Obtaining Formal Models Through Non-Monotonic Refinement (2007)
Parnas, D.L., Madey, J.: Functional Documents for Computer Systems. Science of Computer programming 25(1), 41–61 (1995)
Plagge, D., Leuschel, M.: Seven at One Stroke: LTL Model Checking for High-Level Specifications in B, Z, CSP, and More. Int. Journal on Software Tools for Technology Transfer (1) (2008)
Praxis: Reveal – A Keystone of Modern Systems Engineering. Technical report (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jastram, M., Hallerstede, S., Leuschel, M., Russo, A.G. (2010). An Approach of Requirements Tracing in Formal Refinement. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2010. Lecture Notes in Computer Science, vol 6217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15057-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-15057-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15056-2
Online ISBN: 978-3-642-15057-9
eBook Packages: Computer ScienceComputer Science (R0)