Translating FSP into LOTOS and networks of automata

Andrews T et al (2005) Business process execution language for Web services (WSBPEL). BEA Systems, IBM, Microsoft, SAP AG, and Siebel Systems Astesiano E, Zucca E (1981) Semantics of CSP via translation into CCS. In: Proceedings of the 10th international symposium on mathematical foundations of computer science (MFCS’81). Lecture notes in computer science, vol 118. Springer, Berlin, pp 172–182 Berthomieu B, Bodeveix J-P, Farail P, Filali M, Garavel H, Gaufillet P, Lang F, Vernadat F (2008) FIACRE: an intermediate language for model verification in the TOPCASED environment. In: Laprie J-C (ed) Proceedings of the 4th European congress on embedded real-time software ERTS’08 (Toulouse, France). SIA (the French Society of Automobile Engineers), AAAF (the French Society of Aeronautic and Aerospace), and SEE (the French Society for Electricity, Electronics, and Information and Communication Technologies) Bergamini D, Descoubes N, Joubert C, Mateescu R (2005) BISIMULATOR: a modular tool for on-the-fly equivalence checking. In: Halbwachs N, Zuck L (eds) Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems TACAS’2005 (Edinburgh, Scotland, UK). Lecture notes in computer science, vol 3440. Springer, Berlin, pp 581–585 Bouajjani A, Fernandez J-C, Graf S, Rodríguez C, Sifakis J (1991) Safety for branching time semantics. In: Proceedings of 18th ICALP. Springer, Berlin Berthomieu B, Garavel H, Lang F, Vernadat F (2008) Verifying dynamic properties of industrial critical systems using TOPCASED/FIACRE. ERCIM News 75: 32–33 Bozga M, Graf S, Mounier L (2002) IF-2.0: a validation environment for component-based real-time systems. In: Larsen KG, Brinksma E (eds) Proceedings of the conference on computer-aided verification CAV’2002 (Copenhagen, Denmark). Lecture notes in computer science, vol 2404. Springer, Berlin Basten T, Hooman J (1999) Process algebra in Pvs. In: Proceedings of the 5th international conference on tools and algorithms for the construction and analysis of systems TACAS’99 (Amsterdam, The Netherlands). Lecture notes in computer science, vol 1579. Springer, Berlin, pp 270–284 Brookes SD, Hoare CAR, Roscoe AW (1984) A theory of communicating sequential processes. J ACM 31(3): 560–599 Blom S, Orzan S (2005) Distributed state space minimization. Int J Softw Tools Technol Transf 7(3): 80–291 Brookes SD (1983) On the relationship of CCS and CSP. In: Proceedings of the 10th colloquium automata, languages and programming (ICALP’83). Lecture notes in computer science, vol 154. Springer, Berlin, pp 83–96 Butler M (2000) Csp2B: a practical approach to combining Csp and B. Formal Aspects Comput 12(3): 182–198 Cleaveland R, Madelaine E, Sims S (1995) A front-end generator for verification tools. In: Engberg UH, Larsen KG, Skou A (eds) Proceedings of TACAS’95 tools and algorithms for the construction and analysis of systems (Aarhus, Denmark). Also available as INRIA Research Report RR-2612 Dutertre B, Schneider S (1997) Using a PVS embedding of CSP to verify authentication protocols. In: Proceedings of the 10th international conference on theorem proving in higher order logics TPHOLs’97 (Murray Hill, NJ, USA). Lecture notes in computer science, vol 1275. Springer, Berlin, pp 121–136 Fontaine P, Marion J-Y, Merz S, Nieto LP, Tiu AF (2006) Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems TACAS’06 (Vienna, Austria). Lecture notes in computer science, vol 3920. Springer, Berlin, pp 167–181 Foster H, Uchitel S, Magee J, Kramer J (2005) Tool support for model-based engineering of Web service compositions. In: Proceedings of the IEEE international conference on Web services ICWS’05. IEEE Computer Society Press, Los Alamitos, pp 95–101 Garavel H (1989) Compilation et vérification de programmes LOTOS. Thèse de Doctorat, Université Joseph Fourier (Grenoble) Garavel H (1989) Compilation of LOTOS abstract data types. In: Vuong ST (ed) Proceedings of the second international conference on formal description techniques FORTE’89 (Vancouver B.C., Canada). North-Holland, Amsterdam, pp 147–162 Garavel H (1990) CÆSAR reference manual. Rapport SPECTRE C18, Laboratoire de Génie Informatique, Institut IMAG, Grenoble Garavel H (1998) OPEN/CÆSAR: an open software architecture for verification, simulation, and testing. In: Steffen B (ed) Proceedings of the first international conference on tools and algorithms for the construction and analysis of systems TACAS’98 (Lisbon, Portugal). Lecture notes in computer science, vol 1384. Springer, Berlin, pp 68–84 (full version available as INRIA Research Report RR-3352) Garavel H, Lang F (2001) SVL: a scripting language for compositional verification. In: Kim M, Chin B, Kang S, Lee D (eds) Proceedings of the 21st IFIP WG 6.1 international conference on formal techniques for networked and distributed systems FORTE’2001 (Cheju Island, Korea). IFIP, Kluwer, Dordrecht, pp 377–392 (full version available as INRIA Research Report RR-4223) Garavel H, Lang F, Mateescu R (2002) Compiler construction using LOTOS NT. In: Horspool N (ed) Proceedings of the 11th international conference on compiler construction CC 2002 (Grenoble, France). Lecture notes in computer science, vol 2304. Springer, Berlin, pp 9–13 Garavel H, Lang F, Mateescu R, Serwe W (2007) CADP 2006: a toolbox for the construction and analysis of distributed processes. In: Damm W, Hermanns H (eds) Proceedings of the 19th international conference on computer aided verification CAV’2007 (Berlin, Germany). Lecture notes in computer science, vol 4590. Springer, Berlin, pp 158–163 Garavel H, Serwe W (2006) State space reduction for process algebra specifications. Theor Comput Sci 351(2): 131–145 Groote JF, Vaandrager F (1990) An efficient algorithm for branching bisimulation and stuttering equivalence. In: Patterson MS (eds) Proceedings of the 17th ICALP (Warwick), Lecture notes in computer science, vol 443. Springer, Berlin, pp 626–638 He J, Hoare CAR (2006) CSP is a retract of CCS. In: Proceedings of of the first international symposium on unifying theories of programming (UTP’06). Lecture notes in computer science, vol 4010. Springer, Berlin, pp 38–62 Hennessy M, Li W, Plotkin GD (1981) A first attempt at translating CSP into CCS. In: Proceedings of the second international conference on distributed computing systems (ICDCS’81). IEEE Computer Society Press, Los Alamitos, pp 105–115 Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs ISO/IEC (1989) LOTOS—a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807, International Organization for Standardization—Information Processing Systems—Open Systems Interconnection, Genève ISO/IEC (2001) Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001. International Organization for Standardization—Information Technology, Genève Kavantzas N, Burdett D, Ritzinger G (2004) Web services choreography description language 1.0. W3C. W3C Working Draft Kanellakis PC, Smolka SA (1990) CCS expressions, finite state processes, and three problems of equivalence. Inf Comput 86(1): 43–68 Lang F (2002) Compositional verification using SVL scripts. In: Katoen J-P, Stevens P (eds) Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems TACAS’2002 (Grenoble, France). Lecture notes in computer science, vol 2280. Springer, Berlin, pp 465–469 Lang F (2005) EXP.OPEN 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: van de Pol J, Romijn J, Smith G (eds) Proceedings of the 5th international conference on integrated formal methods IFM’2005 (Eindhoven, The Netherlands). Lecture notes in computer science, vol 3771. Springer, Berlin, pp 70–88 (full version available as INRIA Research Report RR-5673) Lang F (2006) Refined interfaces for compositional verification. In: Najm E, Pradat-Peyre J-F, Viguié Donzeau-Gouge J-F (eds) Proceedings of the 26th IFIP WG 6.1 international conference on formal techniques for networked and distributed systems FORTE’2006 (Paris, France). Lecture notes in computer science, vol 4229. Springer, Berlin, pp 159–174 (full version available as INRIA Research Report RR-5996) Magee J (1999) Behavioral analysis of software architectures using LTSA. In: Proceedings of the 21st international conference on software engineering ICSE’99. ACM Press, London, pp 634–637 Magee J, Dulay N, Eisenbach S, Kramer J (1995) Specifying distributed software architectures. In: Proceedings of the 5th European software engineering conference ESEC’95 (Sitges, Spain). Lecture notes in computer science, vol 989. Springer, Berlin, pp 137–153 Millington M (1987) Theories of Translation Corrections for Concurrent Programming Languages. PhD thesis, LFCS, School of Informatics, University of Edinburgh Milner R (1989) Communication and concurrency. Prentice-Hall, Englewood Cliffs Magee J, Kramer J (1999) Concurrency: state models and Java programs. Wiley, New York Magee J, Kramer J (2006) Concurrency: state models and Java programs, 2006 edn. Wiley, New York Margaria T, Nagel R, Steffen B (2005) Remote integration and coordination of verification tools in JETI. In: Proceedings of the 12th IEEE international conference on the engineering of computer-based systems ECBS’05 (Greenbelt, MD, USA). IEEE Computer Society Press, Los Alamitos, pp 431–436 Mateescu R, Sighireanu M (2003) Efficient on-the-fly model-checking for regular alternation-free Mu-calculus. Sci Comput Programm 46(3): 255–281 Nesi M (1999) Formalising a value-passing calculus in Hol. Formal Aspects Comput 11(2): 160–199 Park D (1981) Concurrency and automata on infinite sequences. In: Deussen P (ed) Theoretical computer science. In: Lecture notes in computer science, vol 104. Springer, Berlin, pp 167–183 Paige R, Tarjan RE (1987) Three partition refinement algorithms. SIAM J Comput 16(6): 973–989 Rushby JM (2006) Tutorial: automated formal methods with PVS, SAL, and Yices. In: Proceedings of the 4th IEEE international conference on software engineering and formal methods SEFM’06 (Pune, India). IEEE Computer Society Press, Los Alamitos, p 262 Salaün G, Bordeaux L, Schaerf M (2006) Describing and reasoning on Web services using process algebra. Int J Business Process Integr Manage 1(2): 116–128 Sighireanu M (2004) LOTOS NT User’s Manual (Version 2.4). INRIA projet VASY. ftp://ftp.inrialpes.fr/pub/vasy/traian/manual.ps.Z, June 2004 Salaün G, Kramer J, Lang F, Magee J (2007) Translating FSP into LOTOS and Networks of Automata. In: Davies J, Schulte W, Song Dong J (eds) Proceedings of the 6th international conference on integrated formal methods IFM’2007 (Oxford, United Kingdom). Lecture notes in computer science, vol 4591. Springer, Berlin, pp 558–578 Salaün G, Serwe W (2005) Translating hardware process algebras into standard process algebras—illustration with CHP and LOTOS. In: van de Pol J, Romijn J, Smith G (eds). In: Proceedings of the 5th international conference on integrated formal methods IFM’2005 (Eindhoven, The Netherlands). Lecture notes in computer science, vol 3771. Springer, Berlin (November 2005. Full version available as INRIA Research Report RR-5666) Salaün G, Serwe W, Thonnart Y, Vivet P (2007) Formal verification of CHP specifications with CADP—illustration on an asynchronous network-on-chip. In: Beerel P, Roncken M, Greenstreet M, Singh M (eds) Proceedings of the 13th IEEE international symposium on asynchronous circuits and systems ASYNC 2007 (Berkeley, California, USA). IEEE Computer Society Press, Los Alamitos, pp 73–82 Tej H, Wolff B (1997) A corrected failure-divergence model for Csp in Isabelle/Hol. In: Proceedings of the 4th international symposium of formal methods Europe FME’97 (Graz, Austria). Lecture notes in computer science, vol 1313. Springer, Berlin, pp 318–337 van Glabbeek RJ, Weijland WP (1989) Branching-Time and Abstraction in Bisimulation Semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989. In: Proceedings of IFIP 11th world computer congress, San Francisco Wang X, Kwiatkowska MZ, Theodoropoulos GK, Zhang Q (2005) Towards a Unifying Csp approach to hierarchical verification of asynchronous hardware. In: Procedings of the 4th international workshop on automated verification of critical systems AVoCS’04 (London, UK). Electronic notes in theoretical computer science (ENTCS) series, vol 128, pp 231–246