Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Algorithm of Translation of MSC-specified System into Petri Net

Kryvyy S., Matvyeyeva L.

Fundamenta Informaticae

2007

Vol. 79, nr 3-4

431-445

We present in this paper the algorithm which performs the translation of MSC'2000 diagrams into Petri net modulo strong bisimulation. The correctness of this algorithm is justified. Here we supplement the MSC'2000 standard with the formal definition of the MSC < condition > element by means of process algebra. This translation algorithm is the part of the automated verification system which formally specifies and verifies a designed software or hardware system specified in the MSC language and is presented in [1] and [2].

Automatic Modeling and Analysis of MSC-specified Systems

Kryvyy S., Matvyeyeva L., Lopatina M.

Fundamenta Informaticae

2005

Vol. 67, nr 1-3

107--120

Formal Methods are a set of methods and tools based on mathematical modeling and formal logic that are used to specify and verify requirements and architecture of hardware or software systems. They can also include means of automatic proving of key properties of designed software or hardware systems. In this paper automatic system is presented which specifies formally and verify designed software or hardware system specified in MSC language. Automatic system is represented as technological process that applies the formal modeling technique of Petri nets and is based on linear algebra methods of analysis, namely, solving the systems of linear equations over the set of natural numbers, in order to research the properties of a system under design. The system is first modeled as a Petri net, and then this model is analyzed. The understanding of the system which results from the analysis will lead to a hopefully errorless system.