fm2011 /
Industry Day
FM 2011 will include an Industry Day that will be dedicated to sharing experience with using formal methods in industrial environments. A draft programme of talks is shown below, and we are now soliciting tools exhibitors.
SCHEDULE HAS BEEN UPDATED
The Industry Day will take place on Wednesday, June 22nd.
INDUSTRY DAY CHAIRS
Andrew Butterfield, Trinity College Dublin, Ireland
Thierry Lecomte, ClearSy, France
LOCATION : KBG13 (Kemmy Business School)
| Registration/Welcome | ||||
11:00 - Keynote Speaker Speaker: Samin Ishtiaq (Microsoft Research, Cambridge) Abstract : Device drivers are a major cause of OS crashes. As device drivers spend much of their time handling queues of requests, many of these errors are related to maintaining memory safety while operating over mutable linked data structures. SLAyer is a program analysis tool designed to prove the absence of memory safety errors such as dangling pointer dereferences, double frees, and memoryleaks. Towards this goal, SLAyer searches for invariants that form proofs in Separation Logic. Complex composite data structures like cyclic doubly-linked lists are supported using parametrized recursive predicates. The algorithms implemented in SLAyer are aimed at verifying moderately sized (10K-30K LOC) systems level code bases written in C. SLAyer is fully automatic and does not require annotations or hints from the programmer. | ||||
| 12:00 - Wei Wei | SAP | Germany | Formal Methods for Business Information Systems | |
 We give an overview of the current formal software engineering practices at SAP for assuring the quality of large business information systems. The topics cover software modeling, formal verification, and model-based testing. On the modeling front, we identify semantic ambiguities in modeling languages such as BPMN, and suggest clarifications that would fit our practical needs. We also investigate scalable modeling methodologies using various decomposition techniques provided by the Rodin platform. For formal verification, we use Rodin/Event-B to examine the layered designs applied to business software development. The goal is to make sure that models at each layer are correctly designed in regard to a number of predefined properties, and that models of different layers are consistent with each other. Finally, we will report on our experiences of using model-based testing to improve the efficiency and coverage of GUI testing through test automation. | ||||
| 12:45 - Lunch | ||||
| 14:00 - Marc Antoni | SNCF | France | Practical formal validation method for interlocking systems | |
 Today, a main question is to answer to the following problematic: have we recognized that for software, the delivery of absolute numerical safety targets is considered to be impossible, and the methods contained in the CENELEC standard produce a probability that certain (unsafe) failure rates will be archived rather than an absolute assurance We know that checks before putting safety signalling facilities into service as well as the results of tests are essential but time consuming without guaranty of exhaustiveness in particular for the case of computerised equipments. In the context of greater economic constraints and increasing complexity of computerized tools, the capacities of the classic approval process are today attained. We see in actual practice a reduction of the validation cover rate and more and more numerous unsafe failures as results. This paper assumes that it is possible in practice to give an exhaustive formal proof that the functional of the signalling application (functional “white box) is safe in the context of use (over-system). The presented method makes it possible, after a rigorous and cost effective design, to validate formally the functional software of critical computerized systems. The aim of our project was to provide the SNCF (today for delegated infrastructure manager, and tomorrow for rolling stock departments of railway undertaker) with an operating method for the formal validation of critical computerized systems, especially for the Interlocking and ETCS/ERTMS systems. A formal proof method by assertion, applicable to these critical systems, which covers equally the specification and its real software implementation, is presented in this paper. With the proposed method and its associated tools we completely verify that the system follows all safety properties at all time and does not show superfluous conditions: it replaces the platform checks and is in accordance with the existing SNCF testing procedures. The advantages are a significant reduction of testing time and of the related costs, an increase of the tests cover rate (deterministic safety vs. probabilistic safety), The paper assumes that the formal methods mastery by infrastructure engineers is a main key to prove that, during the life of the system, more safety is not more expensive. | ||||
| 14:30 - Marc Benveniste | STMicroelectronics | France | Event-B for Correctness and More: A Short Feedback | |
 Two years ago, we reported our experience in the stepwise formal development of a real digital macro-cell, opening the way to the design of digital circuits with zero functional bugs. Since then, we have investigated other uses of the B technology in our application domain, i.e. the design of secure micro-controllers. In this presentation, we briefly recall the particular context of our application domain and the results of 2oo9. Within this context, we explain the real-life limitations of the correctness criteria embedded in our use of the B technology and the extra requirements left uncovered by such formal developments. We provide feedback on experimental work performed to overcome these limitationsi, and we share our present view on the possible adoption of such techniques. This work has been done partially in the frame of the PACA Regional Council ST-focused project “FORmal CO-developMENT”, in a close and fruitful collaboration with Clearsy System Engineering, and partially supported by the MEDEA+ 2A303 BIOP@SS Project. | ||||
| 15:00 - Jean Marc Mota | Thalès | France | Safety formal verification of metro railway signalling systems: feedback from RATP projects. | |
| 15:30 - Coffee Break | ||||
| 16:00 - Aryldo Russo | AeS | Brazil | Doing the same thing better - improving the validation process by the use of formal methods | |
| AeS group has been involved in railway safety critical applications for more than 10 years, and during this time faced a sort of different problems regarding system and software development. In order to tackle these problems AeS group decide, based on evidences collected from the railway domain, to introduce formal methods in its own development process and as a tool to help during assessment projects. As a result, several different projects with formal methods were carried on and a brief description of some of these projects is presented here. To give a better perspective about what is being developed at the moment, a deeper information about the VeRaSys project, Verification of Railway Systems, is also presented. | ||||
| 16:30 - Michael Dierkes | Rockwell Collins | France | Formal Analysis of Aerospace Domain Models in an Industrial Context | |
| For several years, Rockwell Collins has been developing and using a verication framework for MATLAB Simulink and SCADESuite models that can generate input for different proof engines. This verification tool has been used with success for debugging purposes on several industrial case studies, including display and light control systems. Recently, we have used this framework to analyze aerospace domain models containing linear arithmetic computations on reals. In particular, we investigated the properties of a triplex sensor voter, which is a redundancy management unit implemented using linear arithmetic operations as well as conditional expressions (such as saturation). In this presentation, we will give an overview of the Rockwell Collins verification framework, and of some of the industrial case studies it has been applied to in the past. We will then present the recent triplex voter case study and the lessons we learnt from it concerning the verication of models containing real arithmetic, which has been made possible by the progress of modern proof engines. | ||||
| 17:00 - Jean Christophe Deprez | CETIC | Belgium | A FAQ Approach for Collecting Evidence on Formal Method Industrial Usage | |
 After several decades, formal methods are gaining ground in Industry. However, as pointed out by the results of Woodcock et al’s survey, formal methods still need significant additional effort in several areas, most notably in collecting evidence on the use of formal methods and tools in Industry. This article proposes an approach for building a repository of evidence material. The main benefits of the proposed approach are first to make it possible to integrate information for many Industry pilots that have tested diverse formal methods. The secondary benefit is that the current implementation of the approach has a ‘project on a forge’ and of the repository as a wiki of that project is simple yet efficient in managing access and contribution rights. Nonetheless, the shortcomings of the current implementation are also reviewed. | ||||
| Closing/Networking Break | ||||
Tools Exhibitors
Please contact Andrew.Butterfield@lero.ie if you are interested in demoing tools at FM2011
Tool Exhibition Fees
Academic: 100 euro (in addition to I-day registration)
Commercial: 700 euro (includes one I-day registration)
Top
