This special issue contains a selection of the best paper that were presented at the Fourth Workshop on Formal Languages and Analysis of Contract-Oriented Software 1 (FLACOS’10), which was held in Pisa, Italy 17–18 September 2010. The FLACOS workshop series initiated in 2007 as part of (and partially supported by) the Nordunet32 project COSoDIS 3 (“Contract-Oriented Software Development for Internet Services"). The aim of the FLACOS series of workshops has always been to bring together researchers and practitioners working on formal approaches to deal with the different facets of contracts, from synthesis, transformation and refinement to the negotiation, analysis and monitoring of contracts. The program of the FLACOS’10 consisted of 6 regular papers, 6 short papers, and 3 invited papers. The papers were selected by the Programme Committee formed by Björn Bjurling (SICS, Sweden), Antonio Brogi (University of Pisa, Italy, co-chair), Giuseppe Castagna (University Paris 7, France), Suzanne Graf (VERIMAG, France), Alessio Lomuscio (Imperial College London, UK), Ugo Montanari (University of Pisa, Italy), Olaf Owe (University of Oslo, Norway), Gordon Pace (University of Malta, Malta), Ernesto Pimentel (Universidad of Malaga, Spain), Anders P. Ravn (Aalborg University, Denmark), Wolfgang Reisig (Humboldt University, Germany), Kaisa Sere (Abo Akademi, Finland), Gerardo Schneider (Chalmers | University of Gothenburg, Sweden, co-chair), Valentín Valero (University of Castilla-La Mancha, Spain), and Martin Wirsing (LudwigMaximilians University, Germany). Only a few papers were selected with the help of the Programme Committee, and finally only two papers were accepted for publication in this special issue. The first paper, A Trace-based Model for Multi-Party Contracts by Hvitved, Klaedtke and Zalinescu, is concerned with Multiparty contracts. The authors define a model for multi-party contracts in which contract conformance is defined abstractly as a property on traces. Besides it is introduced a contract specification language called CSL which overcomes limitations of previously proposed formalisms for specifying contracts. The approach is illustrated by formalizing various contracts from different domains in CSL. In the second paper accepted for this issue, Synthesis of Secure Adaptors, Martín, Martinelli and Pimentel present an adaptor synthesis, verification and refinement process based on security adaptation contracts, with the aim of overcoming incompatibilities among services and prevents secrecy attacks. They also extend the ITACA toolbox for synthesis and deadlock analysis and integrate it with Crypto-CCS, to verify and refine adaptors based on partial model checking and logical satisfiability techniques.
Formal Languages and Analysis of Contract-Oriented Software (FLACOS'10) -special issue with selected papers
BROGI, ANTONIO;
2012-01-01
Abstract
This special issue contains a selection of the best paper that were presented at the Fourth Workshop on Formal Languages and Analysis of Contract-Oriented Software 1 (FLACOS’10), which was held in Pisa, Italy 17–18 September 2010. The FLACOS workshop series initiated in 2007 as part of (and partially supported by) the Nordunet32 project COSoDIS 3 (“Contract-Oriented Software Development for Internet Services"). The aim of the FLACOS series of workshops has always been to bring together researchers and practitioners working on formal approaches to deal with the different facets of contracts, from synthesis, transformation and refinement to the negotiation, analysis and monitoring of contracts. The program of the FLACOS’10 consisted of 6 regular papers, 6 short papers, and 3 invited papers. The papers were selected by the Programme Committee formed by Björn Bjurling (SICS, Sweden), Antonio Brogi (University of Pisa, Italy, co-chair), Giuseppe Castagna (University Paris 7, France), Suzanne Graf (VERIMAG, France), Alessio Lomuscio (Imperial College London, UK), Ugo Montanari (University of Pisa, Italy), Olaf Owe (University of Oslo, Norway), Gordon Pace (University of Malta, Malta), Ernesto Pimentel (Universidad of Malaga, Spain), Anders P. Ravn (Aalborg University, Denmark), Wolfgang Reisig (Humboldt University, Germany), Kaisa Sere (Abo Akademi, Finland), Gerardo Schneider (Chalmers | University of Gothenburg, Sweden, co-chair), Valentín Valero (University of Castilla-La Mancha, Spain), and Martin Wirsing (LudwigMaximilians University, Germany). Only a few papers were selected with the help of the Programme Committee, and finally only two papers were accepted for publication in this special issue. The first paper, A Trace-based Model for Multi-Party Contracts by Hvitved, Klaedtke and Zalinescu, is concerned with Multiparty contracts. The authors define a model for multi-party contracts in which contract conformance is defined abstractly as a property on traces. Besides it is introduced a contract specification language called CSL which overcomes limitations of previously proposed formalisms for specifying contracts. The approach is illustrated by formalizing various contracts from different domains in CSL. In the second paper accepted for this issue, Synthesis of Secure Adaptors, Martín, Martinelli and Pimentel present an adaptor synthesis, verification and refinement process based on security adaptation contracts, with the aim of overcoming incompatibilities among services and prevents secrecy attacks. They also extend the ITACA toolbox for synthesis and deadlock analysis and integrate it with Crypto-CCS, to verify and refine adaptors based on partial model checking and logical satisfiability techniques.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
