Group on Formal Methods for Industrial Critical Systems
for Computer Science and Technology
Tenth International Workshop on Formal Methods for Industrial
Call for Participation
New University of Lisbon, Lisbon, Portugal
5-6 September 2005
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
- 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
Previous workshops of the ERCIM working group on Formal Methods for Industrial
Critical Systems were held in Oxford (March 1996),
1997), Amsterdam (May
1998), Trento (July 1999),
(April 2000), Paris (July 2001),
(July 2002) , Trondheim (June
2003) and Linz (September
Special event celebrating FMICS's 10th Anniversary
"Ten Commandments Revisited"
A Ten-Year Perspective on the Industrial Application of Formal Methods
Jonathan P. Bowen
London South Bank University
Michael G. Hinchey
NASA Goddard Space Flight Center
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.
ATX Software SA
"The experience of ATX
with the application of formal/rigorous
techniques and methods in real projects"
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
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).
, University of Bonn
analysis of distributed randomized protocols"
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.
NOTE: SUMISSION DEADLINE PASSED
|Deadline for submissions
|15->27 May 2005
|28 June 2005
|Advance Registration Deadline
|1 July 2005
|7 July 2005
|5-6 September 2005
Workshop and Hotel registration
The FMICS 05 registration information will be made available at: http://esecfse05.unl.pt/
| Alvaro Arenas
(Masaryk Univ. Cz)
| Andrew Butterfield
(Dublin Univ., Ie)
|Marsha Chechik (Univ.
of Toronto, Ca)
Fantechi (Univ. of Florence, It)
(NASA gsfc, US)
Huhn (Clausthal Tech. Univ., De)
(Univ. Oldenburg, De)
(CNR/ISTI Pisa, It)
Margaria co-chair (Univ. of Göttingen , De)
co-chair (CNR-ISTI Pisa, It)
(INRIA Rhone-Alpes, Fr)
|Jaco van de
Pol (CWI, Nl)
(Fraunhofer FOKUS, De)
The workshop is organised by the Formal
Methods and Tools Group at CNR-ISTI and by the University of Göttingen.
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
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
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.
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.
Last updated July 7, 2005 at 14:30
Page maintained by