Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: automated verification

Sortuj według:

Ogranicz wyniki do:

Formalization of functional requirements in software development process

Sengupta S., Bhattacharya S.

Foundations of Computing and Decision Sciences

2008

Vol. 33, No. 1

83-115

In this paper, we propose to establish traceability of functional requirements expressed in a SRS document in analysis and design phase that goes down to the coding phase. UML has become a de-facto standard for modeling object-oriented systems. To ensure traceability of requirements in different phases of software lifecycle, it is also mandatory to ensure consistency between different UML diagrams used in those different phases. Here, after specifying some rules to trace requirements and verify consistency, we formally represent functional requirement UML Use case diagram, and some other UML diagrams that are widely used for analyzing and designing object-oriented systems, using Z notation. At the end we represent the formalized functional requirement and the UML diagrams along with their relationship visually using Entity-Relationship (ER) diagram. Implementation of our approach would bridge the gap between a formal language, which is mathematical and difficult to understand and UML that is visual and easy to comprehend. Development of a tool based on this approach would generate a visual representation of formalized functional requirements and their traceability among different UML diagrams, from which automated traceability of requirement in different phases of software development and consistency verification between different UML diagrams can be achieved.

Towards verification of Java programs in VerICS

Orzechowski M., Woźna B., Siwiak T.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

2006

Nr 997

1-33

VerICS has been designed as a tool for automated verification of timed automata, and protocols written in both Intermediate Language and a specification language Estelle. Recently, the tool has been extended to work with so called Timed Automata with Discrete Data and multi-agent systems. The paper presents a prototype of a translator from a subset of the Java programming language to Intermediate Language and Time Automata with Discrete Data, the modeling languages of the VerICS model checker.

Verics został zaprojektowany jako narzędzie do automatycznej weryfikacji automatów czasowych oraz protokołów zapisanych zarówno w języku pośrednim jaki i języku Estelle. Ostatnimi czasy Verics został rozbudowany i obecnie pozwala również na automatyczną weryfikację systemów wieloagentowych oraz protokołów zapisanych za pomocą formalizmu rozszerzonych automatów czasowych. Praca ta opisuje translator z pewnego podzbioru Javy, popularnego ostatnio języka programistycznego, do rozszerzonych automatów czasowych i do języka pośredniego, formalizmów będących językami wejściowymi dla werifikatora Verics.