I-Day sponsored by SAP
|
I-Day sponsored by SAP |
|
University of Newcastle Upon Tyne, Newcastle,
UK
Wednesday 20 July 2005
The theme for I-Day 2005 was "Formal Methods Going Mainstream - Costs, Benefits and Experiences". The purpose of the Industry day is to focus on the perceived pro's and con's of formal methods by end-users, not necessarily the proposition(s) that were made by the technology providers. The aim is really to understand how formal techniques can be introduced successfully in an industrial setting and how common pitfalls can be prevented. Pitfalls, that might not necessarily have anything to do with the formal technique itself. We believe that this information is in particularly valuable for managers, project leaders, system engineers and architects from industry.
Please note that extended abstracts of the invited Industry Day talks can be found in LNCS. Also have a look at the event photos (courtesy of Nico Plat).
|
FM'05 plenary
invited talk by prof. Mathai Joseph |
|
Industry
Day Chaired by mrs. prof. dr. ing.
Tiziana Margaria |
 |
John Harrison
Intel Corporation - USA Floating-point Verification |
|
Only
in a few isolated safety-critical niches of the software industry is any kind
of formal verification widespread. But in the hardware industry, formal
verification is widely practised and increasingly seen as necessary. John
investigates some of the reasons for the difference between these communities
and goes on to show how theorem proving has helped to implement floating point
operations in Intel processors. He will show that theorem proving, with the
help of good tools, has contributed in several ways to the quality of the
product: bugs have been found, potential algorithmic optimizations have been
uncovered and the level of confidence in the implementation and the
intellectual grasp of the problem has been raised. |
 |
John Harrison was a member of the Automated Reasoning Group at the Computer Laboratory of the University of Cambridge. He worked there as a Research Associate and PhD student, supervised by Mike Gordon. After spending a year in the Department of Computer Science of Åbo Akademi University in Finland, he returned to Cambridge as a Research Associate working on Floating Point Verification. Currently, he works for Intel Corporation on this topic. |
 |
Christian Scheidler Daimler Chrysler - Germany Model Checking for Advanced Automotive Applications |
|
Christian
will present the Daimler Chrysler experiences with using state of the art model
checking tools in the automotive industry. The case study that will be
presented was performed in the context of the European project EASIS
(Electronic Architectures and System Engineering for Integrated Safety systems)
and focuses on the development of the advanced automotive assistence system,
which is running on an embedded control unit in a car. The aim of the work is
to investigate to what extend model checking is complimentary to or is a
potential replacement for traditional testing. The case study is performed
using the EmbeddedValidator tool suite, which provides an integrated platform
that couples Matlab/Simulink, dSPACE and two proof engines: VIS and
Prover. |
 |
Christian is a research associate and assistant manager of the Software Technology department at Daimler Chrysler Research and Technology, Germany. He leads the Dependable System Engineering group and his current research activities focuses on systematic testing of powertrain systems, advanced driver assist systems and the use of the Time-Triggered Architecture in the automotive domain. |
 |
Guy H. Broadfoot Verum Consultants - NL ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software |
|
For
many companies, software has become business-critical and software
development is therefore a strategic business activity. At the same time,
traditional software development continues to suffer from poor predictability.
Existing informal techniques seem to have reached a quality ceiling that is
hard if not impossible to break. Formal techniques are needed to reach the next
competence level, but only if they can be combined with existing industrial
methods. Guy presents Analytical Software Design, an approach that bridges the
gap between the informal world of requirements and the formal world of analysis
and synthesis. An overview of ASD will be given and he will present an
industrial case study that was recently completed that shows the significant
impact of the method in practice. |
 |
Guy H. Broadfoot, chief technical officer of Verum Design Consultants, has more than 35 years experience in designing and developing software and software project management in a variety of domains, including operating systems, network software, command and control systems, ship-borne navigation systems, medical imaging, process-control systems and embedded software. He developed the ASD method, for which a British patent application has been submitted. |
 |
Gerrit Muller Embedded Systems Institute - NL The Informal Nature of Systems Engineering |
|
Gerrit
Muller presents a position paper on the relationship between Formal Methods and
Systems Engineering for complex computerized systems. In his opinion, the
meaning of the word "formal" has become overloaded and unclear. He will argue
that Formal Methods are well suited to prescribed homogeneous domains, but that
systems engineering, which integrates more specialized engineering disciplines,
is inherently much more informal. He will use a waferstepper as a typical
example. In this context, he will explain the Systems Engineering discipline.
He will highlight the informal nature of the design process and then goes on to
discuss the relation to Formal Methods. What is the added value of Formal
Methods really? |
 |
Gerrit Muller is Senior Research Fellow at the Embedded Systems Institute and Philips Research. Before that he was manager Systems Engineering at ASML and systems architect at Philips Medical Systems where he worked on waferscanners and MRI & CT scanners respectively. He is well-known for his Gaudí system architecting web-site and courses on the same subject. His research interest includes multi disciplinary design and architectural reasoning for which he developed amongst others the CAFCR model. |
 |
Alexander
Pretschner ETH Zürich - Switserland Model-based Testing in Practice |
|
Model-based testing has attracted a major interest in both academia and
industry. This is not surprising, because testing is an important but above all
a substantial and therefore expensive part of the development process. The
current industrial interest in test-centered development, such as Extreme
Programming, and the gaining momentum of model-based languages and
technologies, such as UML and MDA are certainly contributing factors. Academics
have long attempted to create so-called "lightweight" formal methods,
well-founded techniques that support some part of the design process in a
natural and pragmatic way and model-based testing seems an ideal carrier for
this idea. But despite the appeal of the model-based testing concept, it is not
clear whether the technology really pays off. Alexander takes a critical look
at model-based testing. He will present the perceived promises and benefits and
investigate whether or not there is any acceptable empirical evidence to
support these claims, leading to some provocative observations. |
 |
Alexander Pretschner is a researcher at ETH Zürich. He has worked on industrial projects on model based testing with BMW, EADS-M, Siemens, and Giesecke+Devrient. His research interests include testing, model-based development, information security, and the application of formal methods in the real world, where his focus is on on re-usable test case specifications, modeling methodology and empirical investigations. |
 |
Margus
Veanes (filling in for Wolfram Schulte) Microsoft Research - USA Testing Concurrent Object-Oriented Systems With Spec Explorer |
|
Margus
will describe a practical model-based testing tool developed at Microsoft
Research called Spec Explorer. Spec Explorer enables modeling and automatic
testing of concurrent object-oriented systems. These systems take inputs as
well as provide outputs in form of spontaneous reactions, where inputs and
outputs can be arbitrary data types, including objects. Spec Explorer is being
used daily by several Microsoft product groups. The presented techniques are
used to test operating system components and Web service infrastructure.
Wolfram will give an overview of Spec Explorer tool, the underlying formal
technique and he will also discuss the impact that Spec Explorer has made in
practice at Microsoft. |
 |
Margus is a researcher in the Foundations of Software Engineering group at Microsoft Research since 1999. His research interests are in model-based software development and testing. He has developed model-based testing technology, including efficient search and pruning techniques for exploring infinite state systems, testing of distributed and non-deterministic systems, using game theory and abstract state machines by Yuri Gurevich. He is co-designer of the AsmL Tester tool that is part of AsmL and he has been working closely with Microsoft product groups in bringing this technology into their practice. |
|
|
CLOSING PANEL DISCUSSION with all Industry Day presenters chaired by Tiziana Margaria |
The next ForTIA Industry Day is planned for the FM'06 conference at McMaster University, Canada (21 - 28 August 2006).
Formal Methods Europe (www.fmeurope.org) is an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. FME has been notably successful in bringing together innovators and practitioners in precise mathematical methods for software development, industrial users as well as researchers.
A separate subgroup of FME was recently established, called ForTIA (Formal Techniques Industrial Association, www.fortia.org), which focuses on dissemination of research results and promotion of formal techniques in industry and also to feed lessons learnt from industry back towards academia. ForTIA was founded in 2003 and is currently supported by some 30 companies. One of the key activities of ForTIA is to organize so-called Industry Days, small events targeted at industrial practitioners rather than academics. It is a forum to share experiences on the use of formal techniques in an industrial setting. We invite you to participate in this event.
This page was last updated on 3 August 2005. Contact Marcel dot Verhoef at chess dot nl for any questions concerning the Industry Day 2005.