Preliminary papers :
2000. Pre- and Post-agglomerations for LTL Model Checking. In 21st International Conference on Application and Theory of Petri Nets (ICATPN'00), LNCS vol. 1825, p. 387-408, Springer-Verlag 2000, ISBN:3-540-67693-7. Aarhus, Denmark, jun. 2000.
Abstract : One of the most efficient analysis technique is to reduce an original model into a simpler one such that the reduced model has the same properties than the original one. G. Berthelot defined in this thesis some reductions of Petri nets that are based on local structural conditions and that simplify significantly the net. However, the author focused only on the preservation of classical properties (such that liveness, boundedness, ...) that are not necessarily the most useful in practice. In this paper, we prove that two of these structural reductions (the pre and post transitions agglomerations) preserve also a large set of properties expressed in linear-time temporal logics under simple conditions.
. Automatic Verification of Concurrent Ada Programs. In International Conference on Reliable Software Technologies, Ada-Europe (Ada-Europe'99), LNCS vol. 1622, p. 146-157, Springer-Verlag 1999, ISBN:3-540-66093-3. Santander, Spain, jun. 1999.
Abstract : The behavior of concurrent Ada programs 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. In this paper we present a work based on colored Petri nets 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 allow us to think that we will be able in a near future to analyze realistic Ada program.
. Petri Nets Based Proofs of Ada 95 Solution for Preference Control. In Joint APSEC97/ICSC97 Conference. IEEE CS Press, 1997. Hong-Kong, China, dec. 1997.
Abstract : This paper presents correctness proofs of Ada 95 preference control solution for the dining philosophers paradigm. Preference control is the ability to satisfy a request depending on the parameters passed in by the calling task and often also on the internal state of the server. In Ada 95, this schema is implemented with protected objects, entry families and requeue statements within the protected object. Our aim is to show that the preference control can be described in terms of states and transitions, similar to reactive automaton descriptions. This description, which can be done in terms of colored Petri nets, can lead jointly to validate the chosen implementation and to program it with protected objects and requeue statements of Ada 95. The paper is issued from an examination exercise for our students that have followed a course on Programming and Validation of Concurrent Applications and is presented in form of progressive steps for which the students were expected to give answer. The paper contains three programmed solutions and proofs of absence of deadlock and of starvation.
. Comparing the Reliability Provided by Tasks or Protected Objects for Implementing a Resource Allocating Service : a Case Study. In ACM Tri-Ada International Conference (Tri-Ada'97), p. 51-65, ISBN:0-89791-981-5. Saint-Louis, USA, nov. 1997.
Abstract : We compare two possible implementations of a resource allocation service, one using a task server, the other using a protected object. Both make use of the requeue statement, the count attribute, and also the abort statement in order to satisfy requests, depending on the parameters passed in by the calling task and on the internal state of the service. Because the schema of requeue and entries has an execution semantic based on state and transition, it can be coupled easily with a proof in terms of colored Petri nets. We consider the dining philosophers problem, which is a good illustration of the need for a resource allocation service and for which deadlock- and starvation-free implementations have already been given in Ada95, though not formally proven and sometimes unfair. We give an almost forgotten solution where the dining philosophers problem is safely implemented with protected objects, whereas its implementation with a server task leads to deadlock. We provide two implementations, one of which completes a solution presented by Brosgol in Ada Europe 96 and makes it really fair. Informal proofs are given and are confirmed by Petri nets proofs. Through these examples, we show that the eggshell semantics of protected objects are basic for attaining a reliable implementation.
last update : 30/06/2005