Sciweavers

Share
SIMUTOOLS
2008

Transforming sources to petri nets: a way to analyze execution of parallel programs

8 years 3 months ago
Transforming sources to petri nets: a way to analyze execution of parallel programs
Model checking is a suitable formal technique to analyze parallel programs' execution in an industrial context because automated tools can be designed and operated with very limited knowledge of the underlying techniques. However, the specification must be given using dedicated notations that are not always familiar to engineers (so far, model checking on UML raises complex problems that will not be solved immediately). This paper proposes an approach to perform transformation of source code (C programs) into Petri nets, a suitable specification for model checking. To overcome the complexity of the resulting specification, we focus on specific aspects of the program. So, several transformations can be performed to verify some aspects of the processed programs. Parts of this approach could be reused by intrusion detection systems. Categories and Subject Descriptors D.2 [Software]: Software Engineering; D.2.4 [Software Engineering]: Software / Program Verification--Formal Methods, ...
Jean-Baptiste Voron, Fabrice Kordon
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2008
Where SIMUTOOLS
Authors Jean-Baptiste Voron, Fabrice Kordon
Comments (0)
books