Szczegóły publikacji
Opis bibliograficzny
From extraction of logical specifications to deduction-based formal verification of requirements models / Radosław KLIMEK // W: Software Engineering and Formal Methods : 11th international conference, SEFM 2013 : Madrid, Spain, September 25–27, 2013 : proceedings / eds. Robert M. Hierons, Mercedes G. Merayo, Mario Bravetti. — Berlin ; Heidelberg : Springer-Verlag, cop. 2013. — (Lecture Notes in Computer Science ; ISSN 0302-9743 ; 8137). — ISBN: 978-3-642-40560-0; e-ISBN: 978-3-642-40561-7. — S. 61–75. — Bibliogr. s. 75, Abstr.
Autor
Słowa kluczowe
Dane bibliometryczne
| ID BaDAP | 77244 |
|---|---|
| Data dodania do BaDAP | 2013-10-31 |
| DOI | 10.1007/978-3-642-40561-7_5 |
| Rok publikacji | 2013 |
| Typ publikacji | materiały konferencyjne (aut.) |
| Otwarty dostęp |  |
| Konferencja | 11th International Conference on Software Engineering and Formal Methods |
| Czasopismo/seria | Lecture Notes in Computer Science |
Abstract
The work relates to formal verification of requirements models using deductive reasoning. Elicitation of requirements has significant impact on the entire software development process. Therefore, formal verification of requirements models may influence software cost and reliability in a positive way. However, logical specifications, considered as sets of temporal logic formulas, are difficult to specify manually by inexperienced users and this fact can be regarded as a significant obstacle to practical use of deduction-based verification tools. A method of building requirements models, including their logical specifications, is presented step by step. Requirements models are built using some UML diagrams, i.e. use case diagrams, use case scenarios, and activity diagrams. Organizing activity diagrams into predefined workflow patterns enables automated extraction of logical specifications. The crucial aspect of the presented approach is integrating the requirements engineering phase and the automatic generation of logical specifications. Formal verification of requirements models is based on the deductive approach using the semantic tableaux reasoning method. A simple yet illustrative example of development and verification of a requirements model is provided.
