Working Group on Formal Methods for Industrial Critical Systems

CNR-ISTI Institute for Computer Science and Technology

and

Georg August University of Göttingen

Tenth International Workshop on Formal Methods for Industrial Critical Systems

(FMICS 05)

Call for Participation

New University of Lisbon, Lisbon, Portugal

5-6 September 2005

Co-located with

WORKSHOP PROGRAMME *NEW*

Scope of the workshop

The aim of the FMICS workshop series, which is celebrating its tenth issue, is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops are intended to bring together scientists and practitioners who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications.

Topics include, but are not restricted to:

Tools for the design and development of formal descriptions
Tools for formal verification and analysis of system designs
Verification and validation of complex, distributed, real-time systems and embedded systems
Verification and validation methods that aim at circumventing shortcomings of existing methods in respect to their industrial applicability
Case studies and project reports on formal methods related projects with industrial participation (eg. safety critical systems, mobile systems, object-based distributed systems)
Application of formal methods in standardization and industrial forums

Previous workshops of the ERCIM working group on Formal Methods for Industrial Critical Systems were held in Oxford (March 1996), Cesena (July 1997), Amsterdam (May 1998), Trento (July 1999), Berlin (April 2000), Paris (July 2001), Malaga (July 2002) , Trondheim (June 2003) and Linz (September 2004).

Special event celebrating FMICS's 10th Anniversary

"Ten Commandments Revisited"
A Ten-Year Perspective on the Industrial Application of Formal Methods

Presented by:

Jonathan P. Bowen
London South Bank University
UK

and

Michael G. Hinchey
NASA Goddard Space Flight Center
Greenbelt, MD
USA

Ten years ago, our paper Ten Commandments of Formal Methods suggested some guidelines to help ensure the success of a formal methods project. It proposed ten important requirements (or “commandments”) for formal developers to consider and follow, based on our knowledge of several industrial application success stories, most of which were reported in more detail in [M.G. Hinchey and J.P. Bowen, editors, Applications of Formal Methods, Prentice Hall International Series in Computer Science, Hemel Hempstead, 1995.] and [M.G. Hinchey and J.P. Bowen, editors, Industrial-Strength Formal Methods in Practice, Springer, FACIT series, London, 1999.]. The paper was surprisingly popular, is still widely referenced, and used as required reading in a number of formal methods courses. However, not all have agreed with some of our commandments, feeling that they may not be valid in the long-term.
We re-examine the original commandments ten years on, and consider their validity in the light of a further decade of industrial best practice and experiences.

Invited speakers

Luís Andrade, ATX Software SA

"The experience of ATX with the application of formal/rigorous
techniques and methods in real projects"

Abstract:
ATX offers an integrated set of architectural and re-engineering technologies that, through methods and tools tested in large critical projects, can support long-term strategies of transitioning legacy business functions to core agile services that can sustain crucial competitiveness in the volatile markets of today. Such strategies are being pursued by an increasing number of major IT consumers such as financial institutions, telecoms, and public administration, in response to the need to operate, as first-class players, in the e-Economy.
The fact that the systems in place at these organizations still run on legacy technology (e.g. COBOL) has created the need for re-engineering and enterprise integration technologies.

The solutions that are currently in place are typical based on: internal, labour-intensive migration with low-productivity, high costs and risk or expensive outsourcing to consultancy companies currently using shallow tactical and generalist approaches.
In both cases, these attempts at re-engineering systems are just addressing short-term needs, leading rapidly to a new generation of legacy.

ATX has been working in the architectural structures that can make systems agile and reactive to the way the target business domain will change. Our re-engineering methods and technologies go well beyond the revamping of code. They are based on rigorous and well-established techniques that allow the re-engineering to operate at the level of the business logic and, therefore, align the system architecture with the way markets evolve.

The architectural approach that we will be describing is based on the crucial separation of concerns between: Computation, Coordination, and Configuration. This separation needs to be supported at two different levels. On the one hand, through semantic primitives that address the "business architecture", i.e. the means that need to be provided for modeling business entities (Computation),
the business rules that determine how the entities can interact (Coordination), and the business contexts through which specific rules can be superposed, at run-time, to specific entities (Configuration).

Christel Baier, University of Bonn

"Quantitative analysis of distributed randomized protocols"

Abstract:
A wide range of coordination protocols for distributed systems, internet protocols or systems with unreliable components can formally be modelled by Markov decision processes (MDP). MDPs can be viewed as a variant of state-transition diagrams with discrete probabilities and nondeterminism. While traditional model checking techniques for non-probabilistic systems aims to establish properties stating that all (or some) computations fulfill a certain condition, the verification problem for randomized systems requires reasoning about the quantitative behavior by means of properties that refer to the probabilities for certain computations, for instance, the probability to find a leader within 5 rounds, to deliver a message within 3 attempts along an unreliable channel or the probability for not reaching an error state.

The talk will start with a brief introduction into modelling randomized systems with MDPs and the modelling language ProbMela which is a guarded command language with features of imperative languages, nondeterminism, parallelism, a probabilistic choice operator and lossy channels. The second part of the talk will summarize the main steps for a quantitative analysis of MDP for given temporal logical specifications. The last part will report on the main features of the partial order reduction approach for MDPs and its
implementation in the model checker LiQuor.

Important dates

NOTE: SUMISSION DEADLINE PASSED

Deadline for submissions		15->27 May 2005
Accept/Reject Notification		28 June 2005
Advance Registration Deadline		1 July 2005
Final Manuscript		7 July 2005
Workshop		5-6 September 2005

Workshop and Hotel registration

The FMICS 05 registration information will be made available at: http://esecfse05.unl.pt/

Programme committee

Alvaro Arenas (CCLRC/RAL, UK)

Lubos Brim (Masaryk Univ. Cz)

Andrew Butterfield (Dublin Univ., Ie)

Marsha Chechik (Univ. of Toronto, Ca)

Alessandro Fantechi (Univ. of Florence, It)

Mike Hinchey (NASA gsfc, US)

Leszek Holenderski (Philips, Nl)

Michaela Huhn (Clausthal Tech. Univ., De)

Hardi Hungar (Univ. Oldenburg, De)

Diego Latella (CNR/ISTI Pisa, It)

Tiziana Margaria co-chair (Univ. of Göttingen , De)

Mieke Massink co-chair (CNR-ISTI Pisa, It)

Radu Mateescu (INRIA Rhone-Alpes, Fr)

Jaco van de Pol (CWI, Nl)

Ina Schieferdecker (Fraunhofer FOKUS, De)

Organisation

The workshop is organised by the Formal Methods and Tools Group at CNR-ISTI and by the University of Göttingen.

Working Group Chair	Stefania Gnesi
Workshop Co-Chair	Tiziana Margaria
Workshop Co-Chair	Mieke Massink

Submissions

Papers submitted to FMICS 05 must be in English and present original research that is unpublished and not be under review elsewhere. Final Proceedings will be published with ACM-SIGSOFT.

High quality papers sent to FMICS are candidate for publication in a special issue of the journal for Software Tools for Technology Transfer (STTT).

Papers submitted to FMICS 05 should be up to 16 pages in llncs format, with a clear abstract and list of keywords, or 10 pages in ACM-SIGSOFT format. Please use the llncs style available at http://www.springeronline.com/sgw/cda/frontpage/0,11855,5-164-2-72376-0,00.html or the ACM format available at http://www.acm.org/sigs/pubs/proceed/template.html. The format should be PDF (Adobe's Portable Document Format), using only vectorial ("Type 1") fonts and not bitmap fonts. Note that the final version of accepted papers must conform to the format of ACM-SIGSOFT proceedings.

In case of acceptance of a paper at least one author must present the contribution at the workshop, otherwise it will be removed from the list of publications.

Please submit your paper electronically via the FMICS05 Conference Service . For further information or any problems with
the service please contact us at: fmics05-chairs followed by "at" followed by isti.cnr.it.

Best paper award

As last year, the European Association of Software Science and Technology will be offering an award to the best FMICS paper.

Venue

Venue Campolide Campus

FMICS 05 will take place at the Campolide campus of the New University of Lisbon, Portugal, September 2005, as a co-located workshop of ESEC/FSE 2005, the fifth joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering.

Supporters


	Georg August University of Göttingen

Printable version

Last updated July 7, 2005 at 14:30
Page maintained by
Mieke Massink