Szczegóły publikacji
Opis bibliograficzny
Deduction-based formal verification of requirements models with automatic generation of logical specifications / Radosław KLIMEK // W: Evaluation of Novel Approaches to Software Engineering : 7th international conference ENASE 2012 : Wrocław, Poland, June 29–30, 2012 : revised selected papers / eds. Leszek A. Maciaszek, Joaquim Filipe. — Berlin ; Heidelberg : Springer, cop. 2013. — (Communications in Computer and Information Science ; ISSN 1865-0929 ; 410). — ISBN: 978-3-642-45421-9; e-ISBN: 978-3-642-45422-6. — S. 157–171
Autor
Słowa kluczowe
Dane bibliometryczne
| ID BaDAP | 79872 |
|---|---|
| Data dodania do BaDAP | 2014-02-21 |
| DOI | 10.1007/978-3-642-45422-6_11 |
| Rok publikacji | 2013 |
| Typ publikacji | materiały konferencyjne (aut.) |
| Otwarty dostęp |  |
| Konferencja | 7th International conference on Evaluation of Novel Approaches to Software Engineering |
| Czasopismo/seria | Communications in Computer and Information Science |
Abstract
his 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.
