Welcome to ICFEM 2015

The 17th International Conference on Formal Engineering Methods

Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. We are interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM 2015 is organised and sponsored by Paris-Sud University and CNAM Paris.

The CNAM

The Seventeenth edition of ICFEM and its affiliated workshops will be hosted by the CNAM (Conservatoire National des Arts et Metiers), situated at the heart of Paris. To get to the conference, you should use entrance situated at:

How to get there

The CNAM is nearby three subway stations: "Arts et Métiers" (lines 3 and 11), "Réaumur - Sébastopol" (line 4), and "Temple" (line 3). You can use the following application to find your way. More information about local transportation facilities can be found on RATP's website or on this interactive map. Please, find below how to get to CNAM from the main airports and train stations near/in Paris.

1. From "Charles de Gaulle" airport

1. if your flight landed in terminal 1 or 3, walk until station "Aéroport Charles de Gaulle 1" of RER B,
2. if your flight landed in terminal 2A, 2C, 2D, 2E or 2F, then walk until station "Aéroport Charles de Gaulle 2 - TGV",
3. if your flight landed in terminal 2G, then first take the free bus shuttle "N2" to get to terminal 2F. Then, walk until station "Aéroport Charles de Gaulle 2 - TGV" of RER B,
4. buy an RER ticket to Paris-section-urbaine and take RER B until "Châtelet-les Halles" station,
5. with the same ticket, take metro line 4 (direction "Porte de Clignancourt") until station "Réaumur - Sébastopol",
6. get off at station "Réaumur - Sébastopol", take the exit "rue Papin" and walk until 2 rue Conté. (*)

2. From Orly airport

1. take Orlyval until "Antony" (you need to buy a ticket before taking Orlyval),
2. buy an RER ticket to Paris-section-urbaine and take RER B until "Châtelet-les Halles" station,
3. with the same ticket, take metro line 4 (direction "Porte de Clignancourt") until station "Réaumur - Sébastopol",
4. get off at station "Réaumur - Sébastopol", take the exit "rue Papin" and walk until 2 rue Conté. (*)

3. From "gare de l'Est" and "gare du Nord"

1. buy a metro ticket and take metro line 4 (direction "Mairie de Montrouge") until station "Réaumur - Sébastopol",
2. get off at station "Réaumur - Sébastopol", take the exit "rue Papin" and walk until 2 rue Conté. (*)

4. From "gare Montparnasse"

1. buy a metro ticket and take metro line 4 (direction "Porte de Clignancourt") until station "Réaumur - Sébastopol",
2. get off at station "Réaumur - Sébastopol", take the exit "rue Papin" and walk until 2 rue Conté. (*)

5. From "gare de Lyon"

1. buy a metro ticket and take metro line 1 (direction "La Défense") until station "Hôtel de Ville",
2. with the same ticket, take metro line 11 (direction "Mairie des Lilas") until station "Arts et Métiers",
3. get off at station "Arts et Métiers", take the exit "rue Conté", and walk until 2 rue Conté.

(*) Note that, if you don't want to walk a lot, you can take metro line 3 with the same ticket (direction "Gallieni") from station "Réaumur - Sébastopol" until station "Arts et Métiers". Then, take the exit "rue Conté", and walk until 2 rue Conté.

Where to stay

There are a lot of hotels in and around Paris ! Here is a (non-exhaustive) list of hotels that are close to CNAM:

For students, good prices can be found on this website: https://www.airbnb.fr.

For the 17th International Conference on Formal Engineering Methods, we will be delighted to welcome three quality invited speakers. Below you will find their short bio and an abstract of their talks:

Pr. Ana Cavalcanti (University of York)

Ana Cavalcanti is a Professor of Software Verification at the University of York, UK and a Royal Society-Wolfson Research Merit Award holder. Her research interests are in the theory and practice of formal methods, with application to industry-strength techniques, including Simulink, SysML, and Java, all with sound integrated semantic foundations based on refinement. She holds a PhD from the University of Oxford. From 1997 to 2002 she was a lecturer in the top Formal Methods group in Brazil at the Universidade Federal de Pernambuco. Later, after moving to the UK, she worked at QinetiQ as a Royal Society Industry Fellow to develop techniques for verification of implementations of control law diagrams. Cavalcanti is now the Chair of the Formal Methods Europe Board, and of the steering committee of the International Colloquium on Theoretical Aspects of Computing.

Dr. Rupak Majumdar (Max Planck Institute for Software Systems)

Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. His research interests are in the verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, logic, and automata theory. Dr. Majumdar received the President's Gold Medal from IIT, Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, a Sloan Foundation Fellowship, an ERC Synergy award, "Most Influential Paper" awards from PLDI and POPL, and several best paper awards (including from SIGBED, EAPLS, and SIGDA). He received the B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur and the Ph.D. degree in Computer Science from the University of California at Berkeley. He serves as Chief Scientist of Quaddra Software, a metadata analytics company.

Dr. Sava Krstic (Intel Corporation)

Sava Krstic has been a research scientist and formal validator at Intel for 10 years. Previously, he worked in Pure Math and Theoretical Computer Science.

The FTSCS Workshop also welcomes a quality invited speaker. Here is his short bio:

Prof. José Meseguer (University of Illinois)

José Meseguer is Professor of Computer Science at UIUC and leads the Formal Methods and Declarative Languages Laboratory. He obtained his Ph.D. in Mathematics at the University of Zaragoza, Spain, in 1975. After post-doctoral stays at the University of Santiago de Compostela, and at the University of California at Berkeley, he joined in 1980 the Computer Science Laboratory at SRI International in Menlo Park, California, where he became a Principal Scientist and Head of the Logic and Declarative Languages Group. He joined the University of Illinois at Urbana-Champaign in 2001. He has worked on the design and implementation of several declarative languages, including the OBJ and Maude languages, on formal specification and verification techniques, on concurrency theory, on formal approaches to object-oriented specification, on parallel software and architectures for declarative languages, and on the logical foundations of computer science using equational logic, rewriting logic, and the theory of general logics.

Tuesday 3rd Nov.

8:00 am	Registration opening
8:45 am - 9:00 am	Welcome to ICFEM 2015
9:00 am - 10:00 am	Invited talk Rupak Majumdar   —   Algorithmic Analysis for Asynchronous Programs
10:00 am - 10:30 am	Coffee break
10:30 am - 12:00 pm	Session 1: Testing Wouter Smeenk, Joshua Moerman, Frits Vaandrager and David N. Jansen Applying Automata Learning to Embedded Control Software Jean-Marie Gauthier, Fabrice Bouquet, Ahmed Hammad and Fabien Peureux A SysML Formal Framework to Combine Discrete and Continuous Simulation for Testing Mahsa Varshosaz, Mohammadreza Mousavi and Harsh Beohar Delta-Oriented FSM-Based Testing
12:00 pm - 1:30 pm	Lunch
1:30 pm - 3:00 pm	Session 2: Formal Analysis Thai Son Hoang, Shinji Itoh, Kyohei Oyama, Kunihiko Miyazaki, Hironobu Kuruma and Naoto Sato Consistency Verification of Specification Rules Oana Fabiana Andreescu, Thomas Jensen and Stéphane Lescuyer Dependency Analysis of Functional Specifications with Algebraic Data Structures Lukas Ladenberger and Michael Leuschel Mastering the Visualization of Larger State Spaces with Projection Diagrams
3:00 pm - 3:30 pm	Coffee break
3:30 pm - 5:30 pm	Session 3: Verification Lina Ye, Philippe Dague and Farid Nouioua A Predictability Algorithm for Distributed Discrete Event Systems Crystal Chang Din, Silvia Lizeth Tapia Tarifa, Reiner Hähnle and Einar Broch Johnsen History-Based Specification and Verification of Scalable Concurrent and Distributed Systems Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser and Alexander Weigl Regression Verification for Programmable Logic Controller Software Pablo Castro, Cecilia Kilmurray and Nir Piterman A Recursive Probabilistic Temporal Logic
7:00 pm	Steering Committee Dinner

Wednesday 4th Nov.

8:30 am	Registration opening
9:00 am - 10:00 am	Invited talk Ana Cavalcanti   —   Can Java ever be Safe ? The hijaC Project
10:00 am - 10:30 am	Coffee break
10:30 am - 12:00 pm	Session 4: Specification and Languages Shaoying Liu, Xi Wang and Weikai Miao Supporting Requirements Analysis using Pattern-Based Formal Specification Construction Hamida Bouaziz, Samir Chouali, Ahmed Hammad and Hassan Mountassir SysML Blocks Adaptation Gabriel Ciobanu and Eneia Nicolae Todoran Continuation Semantics for Concurrency with Multiple Channels Communication
12:00 pm - 1:30 pm	Lunch
1:30 pm - 3:30 pm	Session 5: Formal Proof and Theorem-Proving Sylvie Boldo Formal Verification of Programs Computing the Floating-Point Average Sumesh Divakaran, Deepak D'Souza, Prahladavaradan Sampath, Anirudh Kushwah, Nigamanth Sridhar and Jim Woodcock Refinement-Based Verification of the FreeRTOS scheduler in VCC Hiroyuki Yoshida, Kazuhiro Ogata and Kokichi Futatsugi Formalization and Verification of Declarative Cloud Orchestration Shuling Wang, Naijun Zhan and Liang Zou HHL Prover: An Interactive Theorem Prover for Hybrid Systems
3:30 pm - 4:00 pm	Coffee break
4:00 pm - 5:15 pm	Session 6: Formal Analysis Sidi Mohamed Beillahi, Umair Siddique and Sofiene Tahar Formal Analysis of Power Electronic Systems Olga Kouchnarenko and Jean-Francois Weber Practical Analysis Framework for Component Systems with Dynamic Reconfigurations Dennis Guck, Jip Spel and Marielle Stoelinga DFTCalc: Reliability centered maintenance via fault tree analysis (tool paper)
7:30 pm	Banquet

Thursday, 5th Nov.

8:30 am	Registration opening
9:00 am - 10:00 am	Invited talk Sava Krstic   —   Specification and Analysis of SoC Flows
10:00 am - 10:30 am	Coffee break
10:30 am - 11:30 am	Session 7: Logic based approaches Asankhaya Sharma, Aquinas Hobor and Wei-Ngan Chin Specifying Compatible Sharing in Data Structures Étienne André, Camille Coti and Hoang Gia Nguyen Enhanced Distributed Behavioral Cartography of Parametric Timed Automata
12:00 pm - 1:30 pm	Lunch
1:30 pm - 2:45 pm	Session 8: Modeling Cyrille Valentin Artho, Klaus Havelund, Rahul Kumar and Yoriyuki Yamagata Domain-Specific Languages with Scala Juliana Küster Filipe Bowles, Behzad Bordbar and Mohammed Alwanain A logical approach for behavioural composition of scenario-based models Akram Idani and Yves Ledru B for Modeling Secure Information Systems - the B4MSecure platform (tool paper)
2:45 pm - 3:15 pm	Coffee break
3:15 pm - 4:15 pm	Session 9: Model Checking Jandson S. Ribeiro and Aline Andrade A 3-Valued Contraction Model Checking Game: Deciding on the World of Partial Information Jin Cui, Zhenhua Duan, Cong Tian and Nan Zhang Model Checking of a μC/OS-III Multi-task System with TMSVL

See here for the registration to ICFEM 2015 and/or affiliated Workshops.

Scope of the conference

Submissions related to the following principal themes are encouraged, but any topics relevant to the field of formal methods and their practical applications will also be considered.

• Abstraction and refinement
• Formal specification and modeling
• Program analysis
• Software verification
• Software model checking
• Formal approaches to software testing
• Formal methods for self-adaptive systems, for object and component systems, concurrent and real-time systems, for cloud computing and cyber-physical systems, for software safety, security, reliability and dependability
• Tool development, integration and experiments involving verified systems
• Formal methods used in certifying products under international standards
• Formal model-based development and code generation

This year, ICFEM will have special tracks on application of formal methods in three areas:

• Computer security
• Aeronautics
• Train control systems

Submissions in these topics are especially encouraged. Papers in these areas will be subject to the same rigorous review process as other papers. Accepted special track papers will be organised into special sessions.

Types of contributions

• Research papers (max. 16 pages) describing results of theoretical or experimental research, which must be original, significant, and sound. Submissions to the conference must not have been published or be concurrently considered for publication elsewhere.
• Tool papers (max. 6 pages) describing new tools or new features of existing tools, without necessary giving the theoretical background details. Benchmarks or experiences are strongly encouraged. The tools must be available for use by the reviewers.

Submissions and publication

All contributions to ICFEM'15 have to be submitted electronically in PDF format via easy chair. All submissions have to follow the Springer LNCS paper format.

Click here to submit

General chair

• Fatiha Zaïdi, University of Paris-Sud, France

Program chairs

• Michael Butler, University of Southampton, United Kingdom
• Sylvain Conchon, University of Paris-Sud, France

Steering committee

• Keijiro Araki, Kyushu University, Japan
• Michael Butler, University of Southampton, UK
• Jin Song Dong, National University of Singapore [Chair]
• Jifeng He, East China Normal University, China
• Michael Hinchey, University of Limerick, Ireland
• Shaoying Liu, Hosei University, Japan
• Shengchao Qin, University of Teesside, UK

Workshop chair

• Etienne André, LIPN, U. Paris 13

Local arrangment chair

• Tristan Crolard, CNAM, Paris

Financial chair

• The OCamlPro Company

Program committee

• Etienne André, University of Paris 13, France
• Keijiro Araki, University of Kyushu, Japan
• Frank de Boer, CWI, The Netherlands
• Nikolaj Bjorner, Microsoft Research, US
• Ahmed Bouajjani, University of Paris-Diderot, France
• Michael Butler, University of Southampton, United Kingdom
• Sylvain Conchon, University of Paris-Sud, France
• Tristan Crolard, CNAM, France
• Rémi Delmas, ONERA, France
• Zhenhua Duan, Xidian University, China
• Stefania Gnesi, ISTI-CNR, Italy
• Radu Grosu, Vienna University of Technology, Austria
• Ian Hayes, University of Queensland, Australia
• Rob Hierons, Brunel University, UK
• Michaela Huhn, Technische Universität Clausthal, Germany
• Alexei Illiasov, University of Newcastle, United Kingdom
• Fabrice Kordon, University of Paris 6, France
• Yassine Lakhnech, University of Joseph Fourier, Grenoble, France
• Peter Gorm Larsen, Aarhus University, Denmark
• Pascale Le Gall, Ecole Centrale Paris, France
• Xuandong Li, Nanjing University, China
• Shang-Wei Lin, National University of Singapore, Singapore
• Yang Liu, Nanyang Technological University, Singapore
• Shaoying Liu, University of Hosei, Japan
• Stephan Merz, INRIA Nancy, France
• Mohammad Reza Mousavi, Halmstad University, Sweden
• Shin Nakajima, National Institute of Informatics, Japan
• Manuel Nunez, University Complutense, Madrid
• Jun Pang, University of Luxembourg, Luxembourg
• Jan Peleska, University of Bremen, Germany
• Ion Petre, Åbo Akademi University, Finland
• Shengchao Qin, University of Teesside, UK
• Jaco van de Pol, University of Twente, The Netherlands
• Zongyan Qiu, Peking University, China
• Silvio Ranise, FBK, Italy
• Jing Sun, University of Auckland, New Zealand
• Jun Sun, Singapore University of Technology and Design, Singapore
• Kenji Taguchi, AIST, Japan
• Viktor Vafeiadis, MPI-SWS, Germany
• Wang Yi, Uppsala University, Sweden
• Fatiha Zaïdi, University of Paris-Sud, France
• Gianluigi Zavattaro, University of Bologna, Italia
• Huibiao Zhu, East China Normal University, China

Overview and scope

There is a growing interest in applying formal methods in practice to improve software productivity and quality, but only with a few exceptions, this interest has not been successfully converted into the reality of application. How to enable practitioners to easily and effectively use formal techniques still remains challenging.
The Structured Object-Oriented Formal Language (SOFL) has been developed to address this challenge by providing a comprehensible specification language, a practical modeling method, various verification and validation techniques, and tool support through effective integration of formal methods with conventional software engineering techniques. SOFL integrates Data Flow Diagram, Petri Nets, and VDM-SL to offer a visualized and formal notation for specification construction; a three-step approach to requirements acquisition and system design; specification-based inspection and testing methods for detecting errors in both specifications and programs, and a set of tools to support modeling and verification.
The Modeling, Simulation and Verification Language (MSVL) is a parallel programming language. Its supporting toolkit MSV has been developed to enable us to model, simulate and verify a system in a formal manner.
Following the success of previous SOFL+MSVL workshops, this workshop aims to continuously promote the development and combinations of the SOFL formal engineering method and the formal method MSVL, as well as the applications of their fundamental principles or specific techniques to developing other formal engineering techniques. We expect to bring industrial, academic and government experts of SOFL and MSVL to communicate and to exchange ideas. Researchers, practitioners, tool developers and users, and technology transfer experts are all welcome. The scope of the interest includes, but not limited to, all of the possible issues in relation to SOFL, MSVL, or their applications in both developing other formal engineering techniques and specific software systems.

Topic areas include, but are not limited to:

• Modeling and Specification
• Integration of prototyping and formal specification
• Integration of Agile methods and formal specification
• Specification inspection and verification
• Specification animation
• Automatic transformation
• Specification-based inspection and verification
• Specification-based testing
• Evolution and refinement
• Model checking
• Software process
• Project management
• Service-oriented computing
• Data intensive computing
• Many core parallel computing
• Security of software
• Application
• Semantics
• Software Tools

Important dates

• Paper submission: July 1, 2015
• Acceptance/Rejection notification: August 29, 2015
• Workshop: November 6, 2015
• Camera ready : December 15, 2015

See the workshop website for more details >

News

• A special issue of the Science of Computer Programming journal will be devoted to extended versions of selected papers from FTSCS'15.
• The proceedings will be published in Springer's Communications in Computer and Information Science (CCIS) series.

Overview and scope

There is an increasing demand for using formal methods to validate and verify safety-critical systems in fields such as power generation and distribution, avionics, automotive systems, and medical systems. In particular, newer standards, such as DO-178C (avionics), ISO 26262 (automotive systems), IEC 62304 (medical devices), and CENELEC EN 50128 (railway systems), emphasize the need for formal methods and model-based development, thereby speeding up the adaptation of such methods in industry.
The aim of this workshop is to bring together researchers and engineers who are interested in the application of formal and semi-formal methods to improve the quality of safety-critical computer systems. FTSCS strives to promote research and development of formal methods and tools for industrial applications, and is particularly interested in industrial applications of formal methods. Specific topics include, but are not limited to:

• case studies and experience reports on the use of formal methods for analyzing safety-critical systems, including avionics, automotive, medical, and other kinds of safety-critical and QoS-critical systems
• methods, techniques and tools to support automated analysis, certification, debugging, etc., of complex safety/QoS-critical systems
• analysis methods that address the limitations of formal methods in industry (usability, scalability, etc.)
• formal analysis support for modeling languages used in industry, such as AADL, Ptolemy, SysML, SCADE, Modelica, etc.
• code generation from validated models.

The workshop will provide a platform for discussions and the exchange of innovative ideas, so submissions on work in progress are encouraged.

Important dates

• Paper submission: September 5, 2015
• Acceptance/Rejection notification: October 5, 2015
• Workshop: November 6 and/or 7, 2015

See the workshop website for more details >