Abstract
This work concerns requirements gathering and their formal verification using deductive approach. The approach is based on temporal logic and the semantic tableaux reasoning method. Requirements elicitation is carried out with some UML diagrams. A use case, its scenario and its activity diagram may be linked to each other during the process of gathering requirements. Activities are identified in the use case scenario and then their workflows are modeled using the activity diagram. Organizing the activity diagram workflows into design patterns is crucial and enables generating logical specifications in an automated way. Temporal logic specifications, formulas and properties are difficult to specify by inexperienced users and this fact can be a significant obstacle to the practical use of deduction-based verification tools. The approach presented in this paper attempts to overcome this problem. Automatic transformation of workflow patterns to temporal logic formulas considered as a logical specification is defined. The architecture of an automatic generation and deduction-based verification system is proposed.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison Wesley (1999)
Pender, T.: UML Bible. John Wiley & Sons (2003)
Clarke, E., Wing, J., et al.: Formal methods: State of the art and future directions. ACM Computing Surveys 28(4), 626–643 (1996)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Kazhamiakin, R., Pistore, M., Roveri, M.: Formal verification of requirements using spin: A case study on web services. In: Proceedings of the Second International Conference on Software Engineering and Formal Methods (SEFM 2004), pp. 406–415 (2004)
Eshuis, R., Wieringa, R.: Tool support for verifying uml activity diagrams. IEEE Transactions on Software Engineering 30 (7), 437–447 (2004)
Hurlbut, R.R.: A survey of approaches for describing and formalizing use cases. Technical Report XPT-TR-97-03, Expertech, Ltd (1997)
Barrett, S., Sinnig, D., Chalin, P., Butler, G.: Merging of use case models: Semantic foundations. In: 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pp. 182–189 (2009)
Zhao, J., Duan, Z.: Verification of use case with petri nets in requirement analysis. In: Gervasi, O., Taniar, D., Murgante, B., Laganà, A., Mun, Y., Gavrilova, M.L. (eds.) ICCSA 2009, Part II. LNCS, vol. 5593, pp. 29–42. Springer, Heidelberg (2009)
Cabral, G., Sampaio, A.: Automated formal specification generation and refinement from requirement documents. Journal of the Brazilian Computer Society 14 (1), 87–106 (2008)
Fowler, M.: UML Distilled, 3rd edn. Addison-Wesley (2004)
Cockburn, A.: Writing Effective Use Cases. Addison-Wesley (2001)
Klimek, R., Szwed, P.: Formal analysis of use case diagrams. Computer Science 11, 115–131 (2010)
Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science. Volume B, pp. 995–1072. Elsevier, MIT Press (1990)
Klimek, R.: Introduction to temporal logic. AGH University of Science and Technology Press (1999) (in Polish)
Wolter, F., Wooldridge, M.: Temporal and dynamic logic. Journal of Indian Council of Philosophical Research XXVII(1), 249–276 (2011)
van Benthem, J.: Temporal Logic. In: Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 241–350. Clarendon Press (1993–1995)
Chellas, B.F.: Modal Logic. Cambridge University Press (1980)
Pelletier, F.: Semantic tableau methods for modal logics that include the b and g axioms. Technical Report Technical Report FS-93-01, AAAI (Association for the Advancement of Artificial Intelligence) (1993)
d’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J.: Handbook of Tableau Methods. Kluwer Academic Publishers (1999)
Hähnle, R.: Tableau-based Theorem Proving. ESSLLI Course (1998)
Klimek, R.: Towards formal and deduction-based analysis of business models for soa processes. In: Filipe, J., Fred, A. (eds.) Proceedings of 4th International Conference on Agents and Artificial Intelligence (ICAART 2012), Vilamoura, Algarve, Portugal, February 6-8, vol. 2, pp. 325–330. SciTePress (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klimek, R. (2013). Deduction-Based Formal Verification of Requirements Models with Automatic Generation of Logical Specifications. In: Maciaszek, L.A., Filipe, J. (eds) Evaluation of Novel Approaches to Software Engineering. ENASE 2012. Communications in Computer and Information Science, vol 410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45422-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-45422-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45421-9
Online ISBN: 978-3-642-45422-6
eBook Packages: Computer ScienceComputer Science (R0)