Research Article
Transforming sources to petri nets: a way to analyze execution of parallel programs
@INPROCEEDINGS{10.4108/ICST.SIMUTOOLS2008.3055, author={Jean-Baptiste Voron and Fabrice Kordon}, title={Transforming sources to petri nets: a way to analyze execution of parallel programs}, proceedings={1st International ICST Workshop on Petri Nets Tools and Applications}, publisher={ACM}, proceedings_a={PNTAP}, year={2010}, month={5}, keywords={Petri Nets GCC Software Analysis}, doi={10.4108/ICST.SIMUTOOLS2008.3055} }- Jean-Baptiste Voron
Fabrice Kordon
Year: 2010
Transforming sources to petri nets: a way to analyze execution of parallel programs
PNTAP
ICST
DOI: 10.4108/ICST.SIMUTOOLS2008.3055
Abstract
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.