Abstract
Flaws in requirements may have severe impacts on the subsequent phases of the development flow. However, an effective validation of requirements can be considered a largely open problem.
In this paper, we propose a new methodology for requirements validation, based on the use of formal methods. The methodology consists of three main phases: first, an informal analysis is carried out, resulting in a structured version of the requirements, where each fragment is classified according to a fixed taxonomy. In the second phase, each fragment is then mapped onto a subset of UML, with a precise semantics, and enriched with static and temporal constraints. The third phase consists of the application of specialized formal analysis techniques, optimized to deal with properties (rather than with models).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Model Check
- Linear Temporal Logic
- Linear Time Temporal Logic
- Informal Requirement
- Control Natural Language
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
UML Version 2.1.2., http://www.omg.org/spec/UML/2.1.2/
Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language, vol. 61. Springer, Heidelberg (1978)
Abrial, J.R.: The B-book: Assigning Programs to Meanings. C.U. Press, Cambridge (1996)
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers - Principles, techniques and tools. Addison-Wesley, Reading (1986)
Ambriola, V., Gervasi, V.: On the Systematic Analysis of Natural Language Requirements with CIRCE. Autom. Softw. Eng. 13(1), 107–167 (2006)
Banach, R., Bozzano, M.: Retrenchment, and the generation of fault trees for static, dynamic and cyclic systems. In: Górski, J. (ed.) SAFECOMP 2006. LNCS, vol. 4166, pp. 127–141. Springer, Heidelberg (2006)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Formal Methods in System Design 18(2), 141–163 (2001)
Bertoli, P., Bozzano, M., Cimatti, A.: Symbolic model checking framework for safety analysis, diagnosis, and synthesis. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS, vol. 4428, pp. 1–18. Springer, Heidelberg (2007)
Bozzano, M., Villafiorita, A.: The FSAP/NuSMV-SA Safety Analysis Platform. STTT 9(1), 5–24 (2007)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)
Carrington, D.A., Duke, D.J., Duke, R., King, P., Rose, G.A., Smith, G.: Object-Z: An Object-Oriented Extension to Z. In: FORTE 1989, Amsterdam (NL), pp. 281–296 (1990)
Cavada, R., Cimatti, A., Franzén, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. In: FMCAD, pp. 69–76 (2007)
Church, A.: Logic, arithmetic and automata. In: Proc. 1962 Int. Congr. Math., Upsala, pp. 23–25 (1963)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model checker. STTT 2(4), 410–425 (2000)
Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 52–67. Springer, Heidelberg (2008)
Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean Abstraction for Temporal Logic Satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 532–546. Springer, Heidelberg (2007)
Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Object models with temporal constraints. In: SEFM (2008) (to appear)
Cimatti, A., Roveri, M., Tonetta, S.: Syntactic Optimizations for PSL Verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 505–518. Springer, Heidelberg (2007)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Darimont, R., Delor, E., Massonet, P., van Lamsweerde, A.: GRAIL/KAOS: an environment for goal-driven requirements engineering. In: ICSE 1997, pp. 612–613. ACM, New York (1997)
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)
Fantechi, A., Gnesi, S., Ristori, G., Carenini, M., Vanocchi, M., Moreschini, P.: Assisting Requirement Formalization by Means of Natural Language Translation. Formal Methods in System Design 4(3), 243–263 (1994)
Fuxman, A., Liu, L., Mylopoulos, J., Pistore, M., Roveri, M., Traverso, P.: Specifying and analyzing early requirements in Tropos. Requirements Engineering 9(2), 132–150 (2004)
Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Trans. Softw. Eng. Methodol. 5(3), 231–261 (1996)
Nelken, R., Francez, N.: Automatic Translation of Natural Language System Specifications. In: CAV, pp. 360–371 (1996)
OMG. Object Constraint Language: OMG available specification Version 2.0 (2006)
Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC 2006, pp. 821–826 (2006)
Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symp. on Foundation of Computer Science, pp. 46–57 (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th Annual ACM Symposium on Principles of Programming Languages, pp. 179–190 (1989)
Schwitter, R.: Dynamic Semantics for a Controlled Natural Language. In: DEXA Workshops, pp. 43–47 (2004)
Spivey, J.M.: The Z Notation: a reference manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)
Susi, A., Perini, A., Giorgini, P., Mylopoulos, J.: The Tropos Metamodel and its Use. Informatica 29(4), 401–408 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cimatti, A., Roveri, M., Susi, A., Tonetta, S. (2009). From Informal Requirements to Property-Driven Formal Validation. In: Cofer, D., Fantechi, A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2008. Lecture Notes in Computer Science, vol 5596. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03240-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-03240-0_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03239-4
Online ISBN: 978-3-642-03240-0
eBook Packages: Computer ScienceComputer Science (R0)