ISoLA 2007: Poitiers-Futuroscope, France

Yamine Aït Ameur, Frédéric Boniol, Virginie Wiels (Eds.): ISoLA 2007, Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Poitiers-Futuroscope, France, December 12-14, 2007. Revue des Nouvelles Technologies de l'Information RNTI-SM-1 Cépaduès-Éditions 2007, ISBN 978-2-85428-814-8

Invited Talks

Patrick Cousot: Avionic Software Verification by Abstract Interpretation. 1
Paul Caspi: Model-based development of embedded control systems: historical perspective and recent advances. 3
Odile Laurent: The aeronautical systems development challenges for Airbus. 5
Dines Bjørner: Development of Transportation Systems. 7

Ahmed Rahni, Emmanuel Grolleau, Michaël Richard: New worst-case analysis technique for real-time transactions. 9-20
Jean-François Hermant, Laurent George: A C-space sensitivity analysis of Earliest Deadline First scheduling. 21-32
Frédéric Boniol, Claire Pagetti, François Revest: Formal Functionally Deterministic Scheduling. 33-40
Philippe Baufreton, Reinhold Heckmann: Reliable and Precise WCET and Stack Size Determination for a Real-life Embedded Application. 41-48

Nabila Salmi, Patrice Moreaux, Malika Ioualalen: Formal models of Fractal Component Based Systems for performance analysis. 49-60
Cláudia Betous-Almeida, Jean-Luc Scharbarg, Christian Fraboul: Fault-Tolerance Analysis of Mixed CAN/Switched Ethernet Architecture. 61-72

Michael Leuschel, Daniel Plagge: Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more. 73-84
Marco Bakera, Tiziana Margaria, Clemens D. Renner, Bernhard Steffen: Verification, Diagnosis and Adaptation: Tool supported enhancement of the model-driven verification process. 85-97
Jérôme Ermont, Frédéric Boniol: Verification of embbeded systems with preemption: a negative result. 99-110

Andreas Bauer, Martin Leucker, Christian Schallhart, Michael Tautschnig: Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers. 135-146
Mohamed H. Zaki, Sofiène Tahar, Guy Bois: Qualitative Abstraction based Verification for Analog Circuits. 147-158
Jacques Julliand, Hassan Mountassir, Emilie Oudot: Preservation of timed properties during an incremental development by components. 159-166

Sylvain Camier, Damien Chabrol, Vincent David, Christophe Aussaguès: OASIS formal approach for distributed safety-critical real-time system design. 167-178
Joris Rehm, Dominique Cansell: Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method. 179-190

Saddek Bensalem, Moez Krichen, Lotfi Majdoub, Riadh Robbana, Stavros Tripakis: A Simplified Approach for Testing Real-Time Systems Based on Action Refinement. 191-202
Lydie du Bousquet, Masahide Nakamura, Ben Yan, Hiroshi Igaki: Using Formal Methods to increase confidence in one Home Network System implementation: Case study. 203-214
Muzammil Shahbaz, Roland Groz: Using Invariant Detection Mechanism in Black Box Inference. 215-222