For the most recent entries see the Petri Nets Newsletter.

Automatic verification of concurrent Ada program.

Bruneton, E.; Pradat-Peyre, J.-F.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography