In: Lecture Notes in Computer Science, Vol. 1622: Reliable Software Technologies, Ada-Europe'99, pages 146-157. Springer-Verlag, 1999.
Abstract: The behavior of concurrent Ada programs is very is very difficult to understand because of the complexity introduced by multi-tasking. This complexity makes classical test techniques unusable and correctness can only be obtained with the help of formal methods. This paper presents a work based on colored Petri net formalism that automates the verification of concurrent Ada program properties. The Petri net is automatically produced by a translation step and the verification is automatically performed on the net with classical related techniques. A prototype has been developed and first results obtained seem to indicate that realistic Ada programs can be analyzed in the near future.
Keywords: ADA, colored Petri nets, concurrent programming, formal methods, multitasking.
Back to the Petri Nets Bibliography