Format : 15,5x23,5 Reliure : Broché Nombre de pages : 234 Année de parution : 2007 Référence : 814 I.S.B.N. : 978285428814.8 Langue :
Proceedings of the ISoLA workshop On Leveraging Applications of Formal Methods, Verification and Validation. The special theme of the workshop was Formal Methods in Avionics, Space and Transport.
ISoLA is a forum for developers, users, and researchers to discuss issues related to the adoption and use of rigorous tools for the specification analysis, verification, certification, construction, test, and maintenance of systems from the point of view of their di?erent application domains. To bridge the gap between designers and developers of (formal methods based) rigorous tools, and users in engineering and in other disciplines, it fosters and exploits synergetic relationships among scientists, engineers, software developers, decision makers, and other critical thinkers. In particular, by providing a venue for the discussion of common problems, requirements, algorithms, methodologies, and practices, ISoLA aims at supporting researchers in their quest to improve the utility, reliability, ?exibility and e?ciency of tools for building systems and users in their search of adequate solutions to their problems. Applications and case studies with a conceptual message and experience papers with a clear link to tool construction are all encouraged.
Nowadays, it is well accepted that the development of critical systems involves the use of formal methods. The major ?elds where these methods made a lot of progress are the avionics, aerospace and more generally transport areas. Indeed, compared to a previous aircraft generation, the amount of code embedded in a new aircraft generation is continuously increasing. Several methods, tools and techniques have been applied for the development of such systems in di?erent parts of the world and they have been actually put into practice during the development of speci?c aircraft programmes. The aim of this ISoLA workshop is to compile the sate-of-the-art and current research in formal methods applied to the development of avionics and aerospace systems.
The Program Committee chose 15 full technical papers from 25 submissions for presentation at the workshop. Each paper was peer reviewed by three members of the International Program Committee. The Program Committee also selected another 4 papers for inclusion as short papers in the proceedings.
Four keynotes speakers have been invited to share their views on the application of formal methods in the transportation domain. We thank Dines BJORNER, Paul CASPI, Patrick COUSOT and Odile LAURENT for having accepted our invitation.
It has been both a privilege and a pleasure to serve as program committee chairs. Our warmest thanks go to the many individuals and organizations that have helped with this year's workshop. We are very grateful to LISI, ENSMA, university of Poitiers, Airbus France and Easst for their sponsorship and organizational help.
The Steering Committee, the Organizing Committee, and the Program Committee did a marvellous job. Many thanks to all the people explicitly mentioned in the following pages and to all the invisible volunteers that worked hard at making ISOLA 2007 a success. Finally, we want to thank the authors, the presenters and the participants and invite them all to fully enjoy ISOLA 2007, Poitiers and France.
Avionic Software Verification by Abstract Interpretation,
Model-based development of embedded control systems: historical perspective and recent advances,
The aeronautical systems development challenges for Airbus,
Development of Transportation Systems,
New worst-case analysis technique for real-time transactions,
Ahmed Rahni, Emmanuel Grolleau and Michaël Richard
A C-space sensitivity analysis of Earliest Deadline First scheduling,
Jean-François Hermant and Laurent George
Formal Functionally Deterministic Scheduling,
Frédéric Boniol, Claire Pagetti and François Revest
Reliable and Precise WCET and Stack Size Determination for a Real-life Embedded Application,
Philippe Baufreton and Reinhold Heckmann
Formal models of Fractal Component Based Systems for performance analysis,
Nabila Salmi, Patrice Moreaux and Malika Ioualalen
Fault-Tolerance Analysis of Mixed CAN/Switched Ethernet Architecture,
Claudia Betous-Almeida, Jean-Luc Scharbarg and Christian Fraboul
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more,
Michael Leuschel and Daniel Plagge
Veri?cation, Diagnosis and Adaptation: Tool supported enhancement of the model driven veri?cation process,
Marco Bakera, Tiziana Margaria, Clemens D. Renner and Bernhard Ste?en
Verification of embbeded systems with preemption: a negative result,
Jérôme Ermont and Frédéric Boniol
Using Analogy to Promote Conceptual Modeling Reuse,
Karin K. Breitman, Simone D.J. Barbosa, Marco A. Casanova, Antonio L. Furtado AND Michael G. Hinchey
Formal Modeling of Data. A Case Study for Space Applications,
Jean-Paul BLANQUART, Gérard Bulsa, David Lesens, George Mamais and Maxime Perrotin
REFINEMENT / ABSTRACTION METHODS
Don’t care in SMT-Building flexible yet e?cient abstraction/re?nement solvers,
Andreas Bauer, Martin Leucker, Christian Schallhart, and Michael Tautschnig
Qualitative Abstraction based Verification for Analog Circuits,
Mohamed H. Zaki, So?ène Tahar and Guy Bois
Preservation of timed properties during an incremental development by components,
Jacques Julliand, Hassan Mountassir and Emilie Oudot
OASIS formal approach for distributed safety-critical real-time system design,
Sylvain Camier, Damien Chabrol, Vincent David and Christophe Aussaguès
Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method,
Joris Rehm and Dominique Cansell
A Simplified Approach for Testing Real-Time Systems Based on Action Re?nement,