Real-Time and Hybrid Systems

Our research group is involved in the study of the theoretical foundations for the computer aided verification of real-time systems. This research line include among others the study of : timed and hybrid automata, temporal logics and their extension for real-time, ...

Publications :

[1]	Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On model-checking timed automata with stopwatch observers. Information and Computation, 204:408-433, 2006. [ bib ]
[2]	Patricia Bouyer, Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On the optimal reachability problem for weighted timed automata. Journal of Formal Methods in System Design, page 30, 2007 (to appear). [ bib ]
[3]	Véronique Bruyère and Jean-François Raskin. Real-time model-checking: Parameters everywhere. Logical Methods in Computer Science, page 25, 2007 (to appear). [ bib ]
[4]	Véronique Bruyère, Emmanuel Dal'ollio, and Jean-François Raskin. Durations and parametric model-checking in timed automata. Transactions on Computational Logic, page 21, 2007 (to appear). [ bib ]
[5]	Thomas Brihaye, Thomas Henzinger, Vinayak Prabhu, and Jean-François Raskin. Minimum-time reachability in timed games. In Submitted for publication, page 14, 2007. [ bib ]
[6]	Laurent Doyen. Robust parametric reachability for timed automata. Information Processing Letters, page 6, 2007 (to appear). [ bib ]

[1]	Martin De Wulf, Laurent Doyen, and Jean-François Raskin. A lattice theory for solving games of imperfect information. In Proceedings of HSCC 2006: Hybrid Systems-Computation and Control, Lecture Notes in Computer Science. Springer-Verlag, 2006. [ bib | .pdf ]
[2]	Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Automatic rectangular refinement of affine hybrid systems. In Proceedings of FORMATS 2005: Formal Modelling and Analysis of Timed Systems, Lecture Notes in Computer Science 3829, pages 144-161. Springer-Verlag, 2005. [ bib | .pdf ]
[3]	Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Almost ASAP semantics: From timed models to timed implementations. Formal Aspects of Computing, 17(3):319-341, 2005. [ bib | .pdf ]
[4]	Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Systematic implementation of real-time models. In Proceedings of FM 2005: Formal Methods, Lecture Notes in Computer Science 3582, pages 139-156. Springer-Verlag, 2005. [ bib | .pdf ]
[5]	Jean-François Raskin. Handbook of Networked an Embedded Control Systems, chapter An Introduction to Hybrid Automata, pages 491-518. Birkhuser, Springer-Verlag, 2005. [ bib ]
[6]	Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On model-checking timed automata with stopwatch observers. Information and Computation, 2005. To appear. [ bib ]
[7]	Véronique Bruyère, Emmanuel Dal'Ollio, and Jean-François Raskin. Durations and parametric model-checking in timed automata (extended version). Transactions on Computational Logic, 2005. To appear. [ bib | .pdf ]
[8]	Nicolas Markey and Jean-François Raskin. Model-checking restricted sets of timed paths (extended version). Theoretical Computer Science, 2005. To appear. [ bib | .pdf ]
[9]	Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In Proceedings of FORMAT 2005 - Formal Modeling and Analysis of Timed Systems, Third International Conference, number 3829 in Lecture Notes in Computer Science, pages 49-64. Springer-Verlag, 2005. [ bib | .pdf ]

[1]	Nicolas Markey and Philippe Schnoebelen. A PTIME-complete matching problem for SLP-compressed words. Information Processing Letters, 90(1):3-6, January 2004. [ bib | .pdf ]
[2]	Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robustness and implementability of timed automata. In Yassine Lakhnech and Sergio Yovine, editors, Proceedings of the Joint Conferences Formal Modelling and Analysis of Timed Systems (FORMATS'04) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'04), volume 3253 of Lecture Notes in Computer Science, pages 118-133, Grenoble, France, September 2004. Springer. [ bib | .pdf ]
[3]	Nicolas Markey and Philippe Schnoebelen. Symbolic model checking of simply-timed systems. In Yassine Lakhnech and Sergio Yovine, editors, Proceedings of the Joint Conferences Formal Modelling and Analysis of Timed Systems (FORMATS'04) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'04), volume 3253 of Lecture Notes in Computer Science, pages 102-117, Grenoble, France, September 2004. Springer. [ bib | .pdf ]
[4]	François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Model checking timed automata with one or two clocks. In Philippa Gardner and Nobuko Yoshida, editors, Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 387-401, London, UK, August 2004. Springer. [ bib | .pdf ]
[5]	Nicolas Markey and Jean-François Raskin. Model checking restricted sets of timed paths. In Philippa Gardner and Nobuko Yoshida, editors, Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 432-447, London, UK, August 2004. Springer. [ bib | .pdf ]
[6]	Jennifer M. Davoren, Vaughan Coulthard, Nicolas Markey, and Thomas Moor. Non-deterministic temporal logics for general flow systems. In Rajeev Alur and George J. Pappas, editors, Proceedings of the 7th International Conference on Hybrid Systems: Computation and Control (HSCC'04), volume 2993 of Lecture Notes in Computer Science, pages 280-295, Philadelphia, Pennsylvania, USA, March 2004. Springer. [ bib | .pdf ]
[7]	Nicolas Markey and Philippe Schnoebelen. TSMV: A symbolic model checker for quantitative analysis of systems. In Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST'04), pages 330-331, Enschede, The Netherlands, September 2004. IEEE Computer Society Press. [ bib | .pdf ]
[8]	Nicolas Markey. TSMV: model-checking symbolique de systèmes simplement temporisés. In Jacques Julliand, editor, Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 349-352, Besançon, France, June 2004. [ bib | .pdf ]
[9]	Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Almost ASAP semantics: From timed models to timed implementations. In HSCC 04: Hybrid Systems-Computation and Control, Lecture Notes in Computer Science 2993, pages 296-310. Springer-Verlag, 2004. [ bib ]
[10]	Jean-François Raskin. Handbook of Networked and Embedded Control Systems, chapter An Introduction to Hybrid Automata. Springer-Verlag, 2005. [ bib ]
[11]	Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. Model-checking weighted timed automata. In Yassine Lakhnech and Sergio Yovine, editors, Proceedings of FORMATS-FTRTFT'04, number 3253 in Lecture Notes in Computer Science, pages 277-292. Springer-Verlag, 2004. [ bib ]

• Véronique Bruyère, Jean-François Raskin. Real-time Model-checking: Parameters Everywhere !. Accepted for publication in FSTTCS03, 2003. (29 pages) [PDF]
• Véronique Bruyère, Emmanuel Dall'Olio, Jean-François Raskin. Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic. Submitted for publication, 2002. (12 pages) [Postscript]
• Franck Cassez, Thomas Henzinger, and Jean-François Raskin. A Comparison of Control Problems for Timed and Hybrid Systems. Accepted for publication in the proceedings of HSCC'02, Stanford, California. March 2002 (18 pages) [Postscript]
• Thomas Henzinger and Jean-François Raskin. Robust Undecidability of Timed and Hybrid Systems. In proceedings of the Third International Conference on Hybrid Systems: Computation and Control, LectureNotes in Computer Science, 1790, Springer Verlag, pp 145-159, Pittsburgh, USA, March 2000. [Postscript]
• Jean-François Raskin and Pierre-Yves Schobbens. Automata for Qualitative Real-Time. In the proceedings of Les journées montoises de l'informatique théorique, Marnes-La-Vallée, France, March 2000. [Postscript]
• Thomas Henzinger, Jean-François Raskin and Pierre-Yves Schobbens. Axioms for Real-Time Logics (extended version) . Accepted for publication in Theoretical Computer Science, Elsevier Science, 2000. (37 pages) [Postscript]
• Jean-François Raskin and Pierre-Yves Schobbens. The Logic of Event Clocks, Decidability, Complexity,and Expressiveness. In Journal of Automata, Languages and Combinatorics, 4, 3, Otto-von-Guericke-Universität Magdeburg, September 1999. (37 pages) [Postscript]
• Laurent Ferrier, Jean-François Raskin, and Pierre-Yves Schobbens. Models Generation of a Fictitious Clock Real-Time Logic Using Sharing-Trees. In Symbolic Model Checking 99, appeared as Volume 23, Issue 2 of Electronic Notes in Theoretical Computer Science, Trento, Italy, July 1999. [Postscript]
• Jean-François Raskin. Logics, Automata and Classical Theories for Deciding Real Time. Ph. D. Thesis of the Computer Science Department. University of Namur, Belgium, April 1999. (223 pages) [Postscript]
• Jean-François Raskin and Pierre-Yves Schobbens. The Logic of Initially and Next, Complete Axiomatisationand Complexity Issues. In Information ProcessingLetters, 69, Issue 5, pp 221-225, Elsevier Science, March 1999. [Postscript]
• Thomas Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. Axioms for Real-Time Logics. In International Conference on Concurrency, Lecture Notes in Computer Science, 1466, Springer-Verlag, Nice, France, August 1998. [Postscript]
• Thomas Henzinger, Jean-François Raskin and Pierre-Yves Schobbens. The Regular Real-Time Languages. In International Colloquium on Automata, Languages,and Programming, Lecture Notes in Computer Science, 1443, Springer-Verlag, pp 580-591, Aalborg, Denmark, July 1998. [Postscript]
• Jean-François Raskin and Pierre-Yves Schobbens. Real-Time Logics : Fictitious Clock as an Abstraction of Dense Time. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science,  1217, Springer Verlag, pp165-182, Twente,The Netherlands, April 1997. [Postscript]
• Jean-François Raskin and Pierre-Yves Schobbens. State Clock Logic: a Decidable Real-Time Logic .In  Hybrid and Real-Time Systems, Lecture Notes in Computer Science, 1201, Springer Verlag, pp 31-47, Grenoble, France, March 1997. [Postscript]

Concurrent systems can often be abstracted as finite state systems. This makes possible their automatic verification. Unfortunately, such a finite state abstraction does not always exist. If a useful finite state abstraction does not exist, the verification process must consider an infinite state systems. Recently, techniques used to verify finite state systems has been extended, when possible, for the verification of infinite state systems. Our research group is currently working on techniques for the automatic verification of infinite state systems.

Publications :

[1]	Pierre Ganty, Jean-François Raskin, and Laurent Van Begin. A complete abstract interpretation framework for coverability properties of wsts. In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pages 49-64. Springer, 2006. [ bib ]
[2]	Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, enlarge and check: New algorithms for the coverability problem of wsts. J. Comput. Syst. Sci., 72(1):180-203, 2006. [ bib ]
[3]	Alain Finkel, Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the mega-language expressive power of extended petri nets. Theor. Comput. Sci., 356(3):374-386, 2006. [ bib ]
[4]	Jean-François Raskin Gilles Geeraerts and Laurent Van Begin. Well-structured languages. In Submitted for publication, page 35, 2007. [ bib ]
[5]	Pierre Ganty, Jean-François Raskin, and Laurent Van Begin. From many places to few: Automatic abstraction refinement for petri nets. In Submitted for publication, page 25, 2007. [ bib ]

[1]	Giles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 72(1), 2005. 180-203. [ bib | .pdf ]
[2]	Alain Finkel, Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the ω-language expressive power of extended Petri nets. Theoretical Computer Science, 2005. To appear. [ bib | .pdf ]
[3]	Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, enlarge and check... made efficient. In Kousha Etassami and Sriram K. Rajamani, editors, Proceedings of the 17th International Conference on Computer Aided Verification (CAV 05), volume 3576 of LNCS, pages 394-407. Springer, 2005. ISBN 3-540-27231-3. [ bib | .pdf ]
[4]	A. Finkel, Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. A counter-example to the minimal coverability tree algorithm. Technical Report 535, Université Libre de Bruxelles, 2005. 7 pages. [ bib | .pdf ]
[5]	Pierre Ganty, Jean-François Raskin, and Laurent van Begin. A complete abstract interpretation framework for coverability properties of WSTS. In Proc. of Verification, Model Checking and Abstract Interpretation (VMCAI), volume 3855 of Lecture Notes in Computer Science, pages 49-64. Springer-Verlag, 2006. [ bib | .pdf ]
[6]	Javier Esparza, Pierre Ganty, and Stefan Schwoon. Locality-based abstractions. In Proc. of the 12th Int. Symp. on Static Analysis (SAS), volume 3672 of Lecture Notes in Computer Science, pages 118-134. Springer-Verlag, 2005. [ bib | .pdf ]
[7]	Jean-François Raskin and Laurent Van Begin. Games for counting abstractions. In Proceedings AVOCS04, volume 128 of Electronic Notes in Theoretical Computer Science, pages 69-85. Elsevier Science, 2004. [ bib ]
[8]	Thomas Henzinger, Rupak Majumdar, and Jean-François Raskin. A classification of symbolic transition systems. Transactions on Computational Logic, 6(1):1-31, 2005. [ bib | .pdf ]

[1]	Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. In Kamal Lodoya and Meena Mahajan, editors, Proceedings of FSTTCS'04, 24th International Conference on Foundations of Software Technology and Theoretical Computer Science, Chennai, India, number 3328 in Lecture Notes in Computer Science, pages 287-298. Springer-Verlag, 2004. [ bib | .pdf ]
[2]	Alain Finkel, Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the omega-language expressive power of extended Petri nets. In Proceedings of EXPRESS'04, 11th International Workshop on Expressiveness in Concurrency, London, Great Britain, number ?? in Electronic Notes in Theoretical Computer Science. Elsevier Publishing, 2004. [ bib | .pdf ]
[3]	Pierre Ganty and Laurent Van Begin. Non Deterministic Automata for the Efficient Representation of Infinite-state Systems. In Proc. of CP+CV, 1st workshop on Constraint Programming and Constraints for Verification, 2004. [ bib ]
[4]	Jean-François Raskin, Mathias Samuelides, and Laurent Van Begin. Games for Counting Abstraction. In Proceedings of the 4th International Workshop on Verification of Critical Systems (AVOCS 04). Will also appear in ENTCS., 2004. [ bib ]
[5]	Christophe Darlot, Alain Finkel, and Laurent Van Begin. About Fast and TReX accelerations. In Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVOCS 04). will appear in ENTCS., 2004. [ bib ]
[6]	Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. Covering Sharing Trees: Efficient Data Structurs for the Automated Verification of Parametrized Systems. accepted for publication in Software Tools for Technology Transfer Manuscript, 5((2-3)):268-297, 2004. [ bib ]
[7]	Thomas A. Henzinger, Rupak Manjumdar, and Jean-François Raskin. A classification of symbolic transition systems. Transactions on Computational Logic, 6:1-31, 2005. [ bib ]
[8]	Jean-François Raskin and Laurent Van Begin. Petri nets with non-blocking arcs are difficult to analyze. Electronic Notes in Theoretical Computer Science, 98:35-55, 2004. [ bib ]

• Jean-françois Raskin, Mathias Samuelides, and Laurent Van Begin. Petri Games are Monotonic but Difficult to Decide. submitted for publication, 2003. (15 pages) [Postscript]
Alain Finkel, Jean-François Raskin, Mathias Samuelidis, and Laurent Van Begin.
• Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited. In the proceedings of INFINITY'02 to be published as a volume of ENTCS, Brno, 2002. (20 pages) [Postscript]
• Thierry Massart, Jean-françois Raskin, and Laurent Van Begin. Symbolic Distributed Verification of a Class of Parametric Concurrent Systems. In the proceedings of PDMC'02, Brno, 2002. (6 pages) [Postscript]
• Thomas Henzinger, Rupak Manjumdar, and Jean-François Raskin. A Classification of Symbolic Transition Systems. Accepted for publication in TOCL ACM press, 2002 (23 pages). [Postscript]
• M. Leuschel, T. Massart. Logic Programming and Reactive Deduction for the Verification of Reactive Systems: An Experimental Evaluation. In AVoCS'02: Second Workshop on Automated Verification of Critical Systems, Birmingham, April 15-16, 2002
• Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Towards Automated Verification of Multithreaded Java Programs. Accepted for publication in the proceedings of TACAS'02. 2002. [Postscript]
• Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Attacking Symbolic State Explosion in Parametrized Verification. Accepted for publication in CAV'01: International Conference on Computer Aided Verification, Paris, 2001 (11 pages). [Postscript]
• Giorgio Delzanno and Jean-François Raskin. Symbolic Representation of Upward Closed Sets.  In Tools and Algorithms for the Construction and Analysis of Systems,  Lecture Notes in Computer Science, 1785, Springer Verlag, Berlin,Germany,  pp 426-440, March 2000. [Postscript]
• Thomas Henzinger,  Rupak Manjumdar, Freddy Mang, and Jean-François Raskin. Abstract Interpretation of Game Properties. In Seventh International Symposium on Static Analysis, Lecture Note in Computer Science, 1824, Springer Verlag, Santa Barbara, California, pp 220-239, June 2000. [Postscript]
• M. Leuschel, T. Massart.  Infinite State Model Checking by Abstract Interpretation and Program Specialisation.   In 9th International Workshop on Logic-based Program Synthesis and Transformation, Venezia, Italy, LNCS, 1817 , September 1999.

Model Checking

Games

Testing and Monitoring

The impressive growth of heterogeneous networks, especially the Internet, offers new services, such as electronic commerce. Fair exchange and non-repudiation protocols that are at the base of the security of electronic commerce are more complexe than most other
security protocols, as for instance authentication protocols. Hence, they are likely to be even more error-prone. Rencently, we have proposed to use a game semantics to formalize the correctness of exchange protocols and make their computer aided automatic verification possible.

Publications :

[1]	Giorgio Delzanno and Pierre Ganty. Automatic Verification of Time Sensitive Cryptographic Protocols. In Proc. of Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 342-356. Springer-Verlag, 2004. [ bib ]
[2]	Rohit Chadha, Steve Kremer, and Andre Scedrov. Formal analysis of multi-party contract signing. In Proceedings of the 4th IFIP WG1.7 Workshop on Issues in the Theory of Security (WITS'04), Barcelona, Spain, April 2004. [ bib ] We analyze the multi-party contract-signing protocols of Garay and MacKenzie (GM) and of Baum and Waidner (BW). We use a finite-state tool, Mocha, which allows specification of protocol properties in a branching-time temporal logic with game semantics. While our analysis does not reveal any errors in the BW protocol, in the GM protocol we discover serious problems with fairness for four signers and an oversight regarding abuse-freeness for three signers. We propose a complete revision of the GM subprotocols in order to restore fairness.
[3]	Rohit Chadha, Steve Kremer, and Andre Scedrov. Formal analysis of multi-party contract signing. In Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), pages 266-279, Asilomar, Pacific Grove, California, USA, June 2004. IEEE Computer Society Press. [ bib ] We analyze the multi-party contract-signing protocols of Garay and MacKenzie (GM) and of Baum and Waidner (BW). We use a finite-state tool, Mocha, which allows specification of protocol properties in a branching-time temporal logic with game semantics. While our analysis does not reveal any errors in the BW protocol, in the GM protocol we discover serious problems with fairness for four signers and an oversight regarding abuse-freeness for three signers. We propose a complete revision of the GM subprotocols in order to restore fairness.
[4]	Steve Kremer and Mark D. Ryan. Analysing the vulnerability of protocols to produce known-pair and chosen-text attacks. In Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo'04), Electronic Notes in Theoretical Computer Science, London, UK, August 2004. Elsevier Science Publishers. [ bib ] In this paper we report on an analysis for finding known-pair and chosen-text attacks in protocols. As these attacks are at the level of blocks, we extend the attacker by special capabilities related to block chaining techniques. The analysis is automated using Blanchet's protocol verifier and illustrated on two well-known protocols, the Needham-Schroeder-Lowe public-key protocol as well as the Needham-Schroeder symmetric-key protocol. On the first protocol, we show how the special intruder capabilities related to chaining may compromise the secrecy of nonces and that chosen-ciphertext attacks are possible. We propose two modified versions of the protocol which strengthen its security. We then illustrate known-pair and chosen-plaintext attacks on the second protocol.
[5]	Steve Kremer, Aybek Mukhamedov, and Eike Ritter. Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model. In Proceedings of the 9th International Conference on Financial Cryptography and Data Security (FC'05), Lecture Notes in Computer Science, Roseau, The Commonwealth Of Dominica, February-March 2005. Springer. To appear. [ bib ] Multi-party protocol with fairness is a cryptographic protocol allowing several parties to exchange commodities in such a way that everyone gives an item away if and only if it receives an item in return. In this paper we discuss a multi-party fair exchange protocol originally proposed by Franklin and Tsudik, and subsequently shown to have flaws and fixed by González and Markowitch. We identify flaws in a fixed version of the protocol, propose a corrected version, and use strand spaces formal method to prove fairness guarantee of the corrected protocol.
[6]	Steve Kremer and Mark D. Ryan. Analysis of an electronic voting protocol in the applied pi-calculus. In Proceedings of the 14th European Symposium on Programming (ESOP'05), Lecture Notes in Computer Science, Edinburgh, U.K., April 2005. Springer. To Appear. [ bib ] Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO 92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.

• Rohit Chadha, Steve Kremer and Andre Scedrov. Formal analysis of Multi-party Contract Signing. In Workshop on Issues in the Theory of Security (WITS '04), co-located with ETAPS 2004. To appear. Barcelona, Spain. (12 pages) [Postscript]
• Steve Kremer and Jean-François Raskin. Game Analysis of Abuse-free Contract Signing . In Computer Security Foundations Workshop 2002 (CSFW 2002),Cape Breton, Nova Scotia, Canada (15 pages).  [Postscript]
• Steve Kremer and Jean-François Raskin. A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols (Extended Version) . In Journal of Computer Security, Volume 11, Number 3, 2003, pages 399-429. IOS Press(25 pages).  [Postscript]
• Steve Kremer and Jean-François Raskin. A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols . In CONCUR 2001-Concurrency Theory,, Aalborg, Danemark, August 2001 (15 pages).  [Postscript]
• Steve Kremer and Jean-François Raskin. Formal Verification of Non-Repudiation Protocols- A Game Approach . In Formal Methods for Computer Security, Chicago, USA, July 2000 (13 pages).  [Postscript]
• Steve Kremer and Jean-François Raskin. A Game Approach to the Verification of Exchange Protocols - Application to Non-Repudiation Protocols. In Workshop on Issues in the Theory of Security (WITS '00), Geneve, Switzerland, June 2000. (6 pages). [Postscript]

 

Process algebra have been defined to design and specify concurrent systems.  We have studied the properties of process algebra to design systems and also to define "correctness preserving transformations" which allow to synthesize in a semi-automatic way and from an abstract specification, a more refined one so that both systems are linked by a precise refinement relation.  Moreover, in recent works, we have shown how to achieve LTL model-checking using the tool FDR, whose initial purpose is the specification and refinement-checking of CSP processes.

Publications :

• M. Leuschel, I. Wolton, T. Massart, L. Adhianto. Temporal Logic Model Checking of CSP, Tools and Techniques. Proceedings of AVoCS'01: Workshop on Automated Verification of Critical Systems, Oxford, April 19-20, 2001.
• Leuschel, T. Massart, A. Currie.  How to make FDR Spin : LTL Model Checking of CSP by Refinement.   To appear in LNCS Series:  FME'2001, Berlin, Germany, March 2001.
• A. Currie, M. Leuschel, T. Massart.  LTL Model Checking of CSP by Refinement.   In International Workshop on Verification and Computational logic VCL'2000, Lon-don, UK, July 2000.
• T. Massart. A collision Problem in OSI Standard Formal Specification. Journal on Computer Networks and ISDN Systems 26, pp.233-238, 1993.
• T. Massart and R. Devillers. Equality of Agent Expression is Preserved Under an Extension of the Universe of Actions.  Formal Aspect of Computing. 5: 79-88, 1993.
  An abstract is included in Zentralblatt für Mathematik / Mathematics Abstracts.
• T. Massart. A calculus to define correct transformations of LOTOS specifications.In FORTE'91, pp 281-296, 1992.
• T. Massart. An agent calculus with simple actions where the enabling and disabling are derived operators. Information Processing Letters40 pp 213-218, 1991.
• T. Massart. Un calcul algébrique pour définir des raffinements corrects de spécifications LOTOS.  In CFIP'91, pp 465-478, September 1991.