18th International Conference on Formal Engineering Methods
ICFEM 2016
TKP Conference Centre, Tokyo, Japan    14-18 November 2016

Background and Objectives

Since it was started in Hiroshima, Japan in 1997, ICFEM has provided a forum for both researchers and practitioners who are interested in developing practical formal methods for software engineering or applying existing formal techniques to improve software development process in practice. Formal methods for the development of computer systems have been extensively researched and studied. We now have good theoretical understandings of how to describe what programs do, how they do it, and why they work. A range of semantic theories, specification languages, design techniques, verification methods, and supporting tools have been developed and applied to the construction of programs of moderate size that are used in critical applications. The remaining challenge now is how to deal with problems in developing and maintaining large scale and complex computer systems.

The goal of this conference is to bring together industrial, academic, and government experts, from a variety of user domains and software disciplines, to help advance the state of the art. Researchers, practitioners, tool developers and users, and technology transfer experts are all welcome. We are interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical, tangible engineering benefits.

ICFEM 2016 will be organized and sponsored by Hosei University and will be held in the attractive and enjoyable city Tokyo during 14th ~ 18th November 2016. November is one of the two most beautiful and enjoyable seasons in Japan. We are looking forward to your contribution and participation.

Scope and Topics

Submissions related to the following principal themes are encouraged, but any topics relevant to the field of formal engineering methods and their practical applications will also be considered.
  • Abstraction, refinement and evolution
  • Formal specification and modeling
  • Program analysis
  • Formal verification
  • Model checking
  • Formal approaches to software testing and inspection
  • Formal methods for self-adaptive systems
  • Formal methods for object-oriented systems
  • Formal methods for component-based systems
  • Formal methods for concurrent and real-time systems
  • Formal methods for cloud computing
  • Formal methods for cyber-physical systems
  • Formal methods 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

Submission and Publication

Submissions to the conference must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the conference. The proceedings will be published in the Springer Lecture Notes in Computer Science series.

Papers should be written in English and not exceed 16 pages in LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Submission should be made through the ICFEM 2016 submission page (https://easychair.org/conferences/?conf=icfem2016), handled by the EasyChair conference management system.

Workshop or tutorial proposals should be directly sent to the Workshop/Tutorial Chair Shin Nakajima via email. Each proposal should include (1) title, scope, and aims, (2) brief bio of the organizer or lecturer, and (3) postal and email addresses.


Please contact Prof. Shaoying Liu by email at sliu@hosei.ac.jp regarding any issues in relation to registration and payment, and invitation letter.
  1. Each accepted paper must have at least one author registered with the ICFEM 2016 main conference by 29 July 2016. This policy applies to each accepted paper, NOT each author.
  2. Only full-time students are qualified for student registration. A valid evidence, such as the copy of full-time student card or a letter of the student’s supervisor, must be sent by email immediately after the registration and payment are completed.
  3. The main conference fee covers a copy of the proceedings, attendance to all sessions, lunch, and coffee breaks for three days from 16 November to 18 November 2016, and the banquet on 17 November 2016.
  4. The main conference + workshops/tutorial fee covers all of the contents of the main conference mentioned previously. It also covers the attendance to all of the workshops or tutorial available on 14 ~ 15 November as well as lunch and coffee breaks on those two days.
  5. One day workshops/tutorial fee covers the attendance to all of the workshops or tutorial as well as lunch and coffee breaks available only on that day.
  6. All of the registrations and payments should be made using the online registration system. The online registration supports Credit Card payment only. Just in case that the online registration and payment cannot be made for a good reason, other means for payment (wire-transfer, cheque, online-transfer and so on) can be considered. In that case, please contact Prof. Shaoying Liu by email. Registration can only be considered to be complete after the full payment has been received.
  7. All the fees and payments are in Japanese Yen (JPY).
  8. Participants can buy extra conference banquet tickets by 15 November 2016. Each ticket costs 16,000 JPY.
  9. If a participant needs an invitation letter for visa application, please do the registration first and then email Prof. Shaoying Liu for the details.
  10. Registration cancellation policy: Registration fees will be refunded only if the cancellation request is submitted in writing by email no later than midnight October 14, 2016. Cancellations will be subject to a cancellation fee to cover administrative charges. No refunds will be issued for cancellation requests received after October 14, 2016.
Authors’ Registration
Until 29 July 2016
ICFEM main conference (regular) 70,000 JPY
ICFEM main conference (student) 62,000 JPY
ICFEM main conference and workshops/tutorial (regular) 75,000 JPY
ICFEM main conference and workshops/tutorial (student) 65,000 JPY
Workshops/Tutorial only 10,000 JPY

Early Registration
Until 10 September 2016
ICFEM main conference (regular) 70,000 JPY
ICFEM main conference (student) 62,000 JPY
ICFEM main conference and workshops/tutorial (regular) 75,000 JPY
ICFEM main conference and workshops/tutorial (student) 65,000 JPY
Workshops/Tutorial only 10,000 JPY

Late Registration
Until 1 November 2016
ICFEM main conference (regular) 77,000 JPY
ICFEM main conference (student) 68,000 JPY
ICFEM main conference and workshops/tutorial (regular) 82,000 JPY
ICFEM main conference and workshops/tutorial (student) 71,000 JPY
Workshops/Tutorial only 11,000 JPY

On-sight Registration
During 14 ~ 18 November 2016
ICFEM main conference (regular) 80,000 JPY
ICFEM main conference (student) 71,000 JPY
ICFEM main conference and workshops/tutorial (regular) 85,000 JPY
ICFEM main conference and workshops/tutorial (student) 74,000 JPY
Workshops/Tutorial only 15,000 JPY

Extra conference banquet tickets
Until 15 November 2016
One extra conference banquet ticket 16,000 JPY


Preliminary Program for ICFEM 2016 Main Conference

Wednesday, 16 November 2016

9:00 ~ 9:15Opening
9:15 ~ 10:15Keynote Speaker   :   W. Eric Wong

Combinatorial Testing and Its Applications
10:15 ~ 10:45Coffee break
10:45 ~ 12:15[Testing/Symbolic Execution]

Weikai Miao, Geguang Pu, Yinbo Yao, Ting Su, Danzhu Bao and Yang Liu
Automated Requirements Validation for ATP Software via Specification Review and Testing

Takaya Saeki, Fuyuki Ishikawa and Shinichi Honiden
Automatic Generation of Potentially Pathological Instances for Validating Alloy Models

Dominic Scheurer, Reiner Hähnle and Richard Bubel.
A General Lattice Model for Merging Symbolic Execution Branches
12:15 ~ 14:00Lunch
14:00 ~ 16:00[Hybrid/Service-Based Systems]

Ryo Yanase, Tatsunori Sakai, Makoto Sakai and Satoshi Yamane
A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata

Richard Banach and Michael Butler
Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks

Guillaume Babin, Yamine Ait Ameur, Neeraj Kumar Singh and Marc Pantel.
A System Substitution Mechanism for Hybrid Systems in Event-B

Manman Chen, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun and Jin Song Dong
Service Adaptation with Probabilistic Partial Models
16:00 ~16:30Coffee break
16:30 ~ 18:00[Security]

Linas Laibinis, Elena Troubitsyna, Inna Pereverzeva, Ian Oliver and Silke Holtmanns
A Formal Approach to Identifying Security Vulnerabilities in Telecommunication Networks

Minh Hải Nguyễn, Quan Thanh Tho and Le Duc Anh
Multi-Threaded On-the-fly Model Generation of Malware with Hash Compaction

Marco Rocchetto and Nils Ole Tippenhauer
CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions

Thursday, 17 November 2016

9:00 ~ 10:00Keynote Speaker

Tom Maibaum
A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case
10:00 ~ 10:30Coffee break
10:30 ~ 12:30[Formal Verification]

Francesco Marconi, Marcello M. Bersani, Madalina Erascu and Matteo Rossi
Towards the formal verification of data-intensive applications through metric temporal logic

Alexei Iliasov, Alexander Romanovsky and Paulius Stankaitis
Proving Event-B models with reusable generic lemmas

Waqar Ahmed and Osman Hasan
Formal Availability Analysis using Theorem Proving

Akira Tanaka, Reynald Affeldt and Jacques Garrigue
Formal Verification of the rank Algorithm for Succinct Data Structures
12:30 ~ 14:00 Lunch
14:00 ~ 16:00[Concurrency/Distributed Systems]

Brijesh Dongol and Lindsay Groves
Contextual trace refinement for concurrent objects: Safety and progress

Madiel Conserva Filho, Marcel Vinicius Medeiros Oliveira, Augusto Sampaio and Ana Cavalcanti
Local Livelock Analysis of Component-Based Models

Tzu-Chun Chen, Crystal Chang Din and Eduard Kamburjan
Session-Based Compositional Analysis for Actor-Based Languages Using Futures

Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix and Mamoun Filali-Amine
An Event-B development process for the distributed BIP framework
16:00 ~16:30Coffee break
16:30 ~ 17:30Panel Discussion

How can formal methods become effective and acceptable “medicine” for software engineering “diseases”?
18:00 ~ 21:30Banquet (Symphony Tokyo Bay Dinner Cruise)

Friday, 18 November 2016

9:00 ~ 10:00Keynote Speaker

Keijiro Araki
Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa's Case
10:00 ~ 10:30Coffee break
10:30 ~ 12:30[Model Checking]

Shuanglong Kan
Partial Order Reduction for State/Event Systems

Peizun Liu and Thomas Wahl
Concolic Unbounded-Thread Reachability via Loop Summaries

Truong Khanh Nguyen, Tian Huat Tan, Jun Sun, Jiaying Li, Yang Liu, Manman Chen and Jin Song Dong
Making Use of Simulation Techniques in Verifying Timed System

Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Félix Ingrand and Anthony Mallet
Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots
12:30 ~ 14:00 Lunch
14:00 ~ 15:30[Real-Time Systems]

Étienne André, Didier Lime and Olivier H. Roux
Decision Problems for Parametric Timed Automata

Saurabh Gadia, Cyrille Valentin Artho and Gedare Bloom
Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder

Min Zhang, Frederic Mallet and Huibiao Zhu
An SMT-based Approach to the Formal Analysis of MARTE/CCSL
15:30 ~ 16:00Coffee break
16:00 ~ 17:00[Formal Analysis]

Nuno Amalio, Richard Payne, Ana Cavalcanti and Jim Woodcock
Checking SysML Models for Co-Simulation

Manuel Toews and Heike Wehrheim
A CEGAR Scheme for Information Flow Analysis
17:00 ~ 17:15Closing

Click here to download pdf file of program.


There are many hotels in Tokyo from which you can quickly and easily access the conference venue by the public transportation, but the following list gives a few hotels near the conference venue. November is one of the best seasons in Japan and hotels tend to be very busy. If you plan to attend the conference, it will be good if you can book your hotels as early as you can. For hotel reservation, please directly use the hotel webpages or directly contact with the hotels.

・Hotel Grand Hill

・Arkadia Ichigaya

・APA Hotel Tokyo-Kudanshita

・Hotel Monterey Hanzomon

・Hotel metropolitan Edmont

・Tokyo Dome Hotel

・Flexstay Inn Iidabashi


The conference will be held at the TKP Ichigaya Conference Centre in Tokyo.

Name:TKP Ichigaya Conference Center
Address:8 banchi, Ichigayahachimancho, Shinjuku-ku, Tokyo, 162-0844

Access to Ichigaya Station :

Important Dates

Abstract Submissions Due :22 April 2016
Full Paper Submissions Due:7 May 2016
Workshop/Tutorial Proposals Due:25 March 2016
Acceptance / Rejection Notification:29 June 2016  
Camera-ready Papers Due:29 July 2016  

All of the authors who submit their abstracts of full papers by 1st April 2016 will receive a special Japanese gift when they come to attend the conference with ICFEM 2016 main conference registration.

Keynote Speakers

W. Eric Wong (University of Texas at Dallas)


Combinatorial Testing and Its Applications


Studies have shown that combinatorial testing can help programs detect hard-to-find software bugs that may not be revealed by test cases generated using other testing techniques. The first part of this talk focuses on traditional black-box requirements-based combinatorial testing. In particular, I will discuss results and lessons learned from two real-life industry applications: a control panel of a rail-road system and a Linux system. The second part extends the concept of combinatorial testing to a white-box structure-based setting. I will present an advanced coverage criterion, Combinatorial Decision Coverage, in conjunction with symbolic execution to achieve high coverage cost-effectively without suffering from potential space exploration. Finally, I will explain how combinatorial testing can be applied to a graph-based methodology for testing IoT (Internet of Things).


W. Eric Wong received his M.S. and Ph.D. in Computer Science from Purdue University, West Lafayette, Indiana, USA. He is a Full Professor, the Director of International Outreach, and the Founding Director of Advanced Research Center for Software Testing and Quality Assurance ( http://paris.utdallas.edu/stqa) in Computer Science at the University of Texas at Dallas (UTD). He also has an appointment as a guest researcher at the National Institute of Standards and Technology, an agency of the U.S. Department of Commerce. Prior to joining UTD, he was with Telcordia Technologies (formerly Bellcore) as a senior research scientist and the project manager in charge of Dependable Telecom Software Development.

Dr. Wong is the recipient of the 2014 IEEE Reliability Society Engineer of the Year. He is also the Edit-in-Chief of the IEEE Transactions on Reliability. His research focuses on helping practitioners improve software quality while reducing production cost. In particular, he is working on software testing, program debugging, risk analysis, safety, and reliability. Dr. Wong has published more than 180 papers and edited 2 books.

Dr. Wong is also the Founding Steering Committee Chair of the IEEE International Conference on Software Security and Reliability (SERE) and the IEEE International Workshop on Program Debugging. In 2015, the SERE conference and the QSIC conference (International Conference on Quality Software) merged into one large conference, QRS, with Q representing Quality, R for Reliability, and S for Security. Dr. Wong continues to be the Steering Committee Chair of this new conference (http://paris.utdallas.edu/qrs).

Keijiro Araki (Kyushu University)


Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa's Case


We have been making much efforts to promote formal methods in Japan, especially Japanese IT campanies. I report our activities in Japan for almost twenty years, and show typical reactions of those Japanese companies to application of formal methods. I mention about the obstacles they think to adopting formal methods in their real software development projects. On the other hand I also present a case of FeliCa Networks, Inc. as a best practice of applying formal methods in Japan. I discuss the lessons learned from our efforts of promoting formal methods and the FeliCa's case. Finally, I briefly introduce our research project to support software developpers in adopting formal approaches to real projects.


Keijiro Araki is a Distinguished Professor of Kyushu University, where he is also serving as Dean of Graduate School of Information Science and Electrical Engineering, Director of Ito Library, and Director of Research Center for Architecture Oriented Formal Methods. He is Member of Science Council of Japan since 2006. He served as IEEE Fukuoka Section Chair, Chair of IPSJ (Information Processing Society of Japan) Kyushu Chapter, Chair of Kyushu Chapter of the Society of Project Management, and so on. He has been contributing to international academic events such as Organizing Chair of IEEE TENCON 2010, Organizing Chair of ICFEM 2008, Program Chair of ICTAC 2004, Program Chair of FM 2003, and Program Chair of IFM 99. His research interests include formal approaches to software development, formal modelling of software systems, verification & validation of embedded systems, and so on.

Tom Maibaum (McMaster University)


A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case


The use of safety (assurance) cases was a step in the right direction when it comes to safety assurance. In particular, they make a serious attempt to explicate and to provide some structure for the reasoning involved in assuring that a system is safe, generally in terms of so called arguments. Currently, the notations used for the statement of safety cases have no formal semantics and are loosely linked to goal structured notations and Toulmin’s concept of argument. Historically, it has been clearly demonstrated that languages that have no formal semantics are deficient in relation to the requirements of a serious approach to engineering, as the ability to analyze and confidence in the result both require the precision of a formal semantics. One can only go so far with intuition, certainly not far enough to justify complex system safety, as for Cyber Physical Systems and autonomous cars. By rehearsing Gentzen’s program for formalizing mathematical reasoning by developing his Natural Deduction approach, we show how we can begin our program of formalizing safety reasoning and we develop a working definition of a safety reasoning formalism.

In the context of safety cases, evidence plays a prominent role and presents a strong, and equally challenging, starting point for discussion. Evidence is what grounds the claims in a safety case and speaks to their plausibility; it is what separates the arguments linking the claims in a safety case from arguments that are purely deductive. All in all, the very idea of evidence in safety arguments presents an interesting topic for research, more so, as it is one with immediate practical implications for safety praxis. We use analogies with reasoning in science and law to characterize the role played by evidence in safety cases. By way of illustration of our approach to a formal semantics for safety reasoning, we offer some thoughts on evidence, the place it occupies in safety cases, and some of the challenges that this notion presents. We illustrate the ideas with an example from the literature, which we reformulate on the basis of our principles.

Conference Organizing Committee

General Chair

  • Shaoying Liu, Hosei University, Japan

Program Chairs

  • Kazuhiro Ogata, JAIST, Japan
  • Mark Lawford, McMaster University, Canada

Workshop/Tutorial Chair

  • Shin Nakajima, NII, Japan

Publicity Chair

  • Kenji Taguchi, AIST, Japan

Local Arrangement Chair

  • Fumiko Nagoya, Nihon University, Japan

Web Chair

  • Hayato Ikeda, Hosei University, Japan

Program Committee

  • Bernhard Aichernig, University of Graz, Austria
  • Étienne André, University of Paris 13, France
  • Toshiaki Aoki, JAIST, Japan
  • Christian Attiogbe, University of Nantes, France
  • Richard Banach, University of Manchester, United Kingdom
  • Ezio Bartocci, TU Wien, Austria
  • Michael Butler, University of Southampton, United Kingdom
  • Ana Cavalcanti, University of York, United Kingdom
  • Sungdeok Cha, Korea University, Korea
  • Yuting Chen, Shanghai Jiaotong University, China
  • Sylvain Conchon, University of Paris-Sud, France
  • Frank De Boer, CWI, Netherlands
  • Zhenhua Duan, Xidian University, China
  • Jeremy Gibbons, University of Oxford, United Kindom
  • Stefania Gnesi, ISTI-CNR, Italy
  • Lindsay Groves, Victoria University of Wellington, New Zealand
  • Ian J. Hayes, University of Queensland, Australia
  • Michaela Huhn, Technische Universität Clausthal, Germany
  • Alexei Iliasov, University of Newcastle, United Kingdom
  • Fuyuki Ishikawa, NII, Japan
  • Weqiang Kong, Dalian University of Technology, China
  • Fabrice Kordon, University of Paris 6, France
  • Xiaoshan Li, University of Macau, China
  • Yang Liu, Nanyang Technological University, Singapore
  • Larissa Meinicke, University of Queensland, Australia
  • Stephan Merz, INRIA Nancy, France
  • Huaikou Miao, Shanghai University, China
  • Mohammadreza Mousavi, Halmstad University, Sweden
  • Shin Nakajima, NII, Japan
  • Akio Nakata, Hiroshima City University, Japan
  • Manuel Nuñez, Complutense University of Madrid, Spain
  • Kozo Okano, Shinshu University, Japan
  • Jun Pang, University of Luxembourg, Luxembourg
  • Jan Peleska, University of Bremen, Germany
  • Ion Petre, ÁEo Akademi University, Finland
  • Shengchao Qin, Teesside University, United Kingdom
  • Silvio Ranise, FBK, Italy
  • Adrian Riesco, Complutense University of Madrid, Spain
  • Jing Sun, University of Auckland, New Zealand
  • Kenji Taguchi, AIST, Japan
  • Jaco Van De Pol, University of Twente, Netherlands
  • Thomas Wahl, Northeastern University, USA
  • Xi Wang, Shanghai University, China
  • Alan Wassyng, McMaster University, Canada
  • Fatiha Zaidi, University of Paris-Sud, France
  • Jian Zhang, Chinese Academy of Sciences, China
  • Min Zhang, East China Normal University, China
  • Hong Zhu, Oxford Brookes University, United Kingdom
  • Huibiao Zhu, East China Normal University, China

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
  • Mike Hinchey, University of Limerick, Ireland
  • Shaoying Liu, Hosei University, Japan
  • Shengchao Qin, University of Teesside, UK



Paper submissionNotificationWorkshop
SOFL+MSVLAugust 1, 2016August 31, 2016November 15, 2016
FTSCS September 4, 2016October 7, 2016November 14/15, 2016
FM&MMDSeptember 20, 2016October 16, 2016November 14, 2016


CafeOBJNovember 15, 2016 (one day)


Background and Objectives:

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.

Important dates:

Paper submission:1st August 2016
Acceptance/Rejection notification:31th August 2016
Workshop:15th November 2016
Camera ready paper due:23th December 2016


Topic areas:

Topic areas include, but are not limited to:
  1. Modeling and Specification
  2. Integration of prototyping and formal specification
  3. Integration of Agile methods and formal specification
  4. Specification inspection and verification
  5. Specification animation
  6. Automatic transformation
  7. Specification-based inspection and verification
  8. Specification-based testing
  9. Evolution and refinement
  10. Model checking
  11. Software process
  12. Project management
  13. Service-oriented computing
  14. Data intensive computing
  15. Many core parallel computing
  16. Security of software
  17. Application
  18. Semantics
  19. Software Tools

Keynote Speaker:

Prof. Huaikou Miao, Shanghai University, China


All submissions will be reviewed by program committee members on the basis of technical quality, relevance, significance, and clarity; and those accepted will be published in the workshop proceedings. Technical papers should describe original research, and industrial experience should include practical projects and analysis emphasizing outcomes, insights gained, and lessons learned.
All authors should submit papers via the online EasyChair system https://www.easychair.org/conferences/?conf=soflmsvl2016. Submitted manuscripts must be written in English and should be no longer than 20 pages in Springer’s LNCS format described at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0. Authors of accepted papers will have to submit the final camera-ready papers via the EasyChair system and sign a copyright release form. The workshop proceedings will be published as an LNCS post-proceedings by Springer.

General Chairs

  • Shaoying Liu, Hosei University, Japan
  • Zhenhua Duan, Xidian University, China

Program Co-Chairs

  • Cong Tian, Xidian University, China
  • Fumiko Nagoya, Nihon University, Japan

Program Committee

  • Yuting Chen, Shanghai Jiaotong University, China
  • Zhenhua Duan, Xidian University, China
  • Stefan Gruner, University of Pretoria, South Africa
  • Gihwon Kwon, Kyonggi University, Korea
  • Richard Lai, La Trobe University, Australia
  • Karl Leung, Hong Kong Institute of Vocational Education
  • Guoqiang Li, Shanghai Jiaotong University, China
  • Xiaohong Li, Tianjin University, China
  • Shaoying Liu, Hosei University, Japan
  • Weikai Miao, East China Normal University, China
  • Shin Nakajima, National Institute of Informatics (NII), Japan
  • Fumiko Nagoya, Nihon University, Japan
  • Kazuhiro Ogata, JAIST, Japan
  • Shengchao Qin, Teesside University, UK
  • Wuwei Shen, Western Michigan University, USA
  • Jing Sun, University of Auckland, New Zealand
  • Cong Tian, Xidian University, China
  • Xi Wang, Shanghai University, China
  • Xinfeng Shu, Xi'an University of Posts and Telecommunications, China
  • Xiaobing Wang, Xidian University, China
  • Haitao Zhang, Lan Zhou University, China
  • Hong Zhu, Oxford Brookes University, UK


Background and Objectives:

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.

Important dates:

Paper submission:September 4, 2016
Notification:October 7, 2016
Workshop:November 14/15, 2016

See the workshop website for more details >


Background and Objectives:

Development of trustworthy software-intensive systems constitutes one of the major engineering challenges. Both functional correctness and extra-functional properties such as safety, reliability and security are equally important for ensuring system trustworthiness. To efficiently cope with complexity caused by inherently heterogeneous development environment, the designers often rely of model-driven techniques that provide them with a comprehensive integrated notation. Indeed, graphical models help to bridge the gap between informal requirements and formal models, while various architectural modelling frameworks enable the efficient multi-view analysis of diverse system properties.

Though the benefits of using both formal and model-driven techniques in the design of trustworthy systems are widely acknowledged, there is still a lack of common understanding of the integration mechanisms. In particular, there are the on-going debates about achieving a balance between flexibility and rigour in integrated modelling, analysing an interplay between functional and extra-functional properties, using domain-specific frameworks as well as addressing trustworthiness at different architectural levels.

Important dates:

Paper submission:September 13, 2016
Notification:October 16, 2016
Final papers:November 2, 2016
Workshop:November 14, 2016

See the workshop website for more details >


Title:A tutorial on formal specification and verification with CafeOBJ
Lecturers:Kokichi Futatsugi and Kazuhiro Ogata, JAIST, Japan
Day(s):15th November 2016 (one day)

Background and Objectives:

This tutorial allows participants to learn some recently developed functionalities and verification techniques, such as CafeOBJ CITP (a proof assistant for CafeOBJ) and the generate & check method, as well as some matured concepts and techniques to specify and verify software systems, such as signatures, equations and proof scores, with some concrete examples, such as natural numbers and simple mutual exclusion protocols. The tutorial begins with some basic concepts, such as sorts, operators and equations, uses some concrete simple examples as written, and then does not require any knowledge of formal methods. Some basic concepts in mathematics, such as sets and functions, and/or some experiences on programming can help participants get better understandings of the technical contents of the tutorial.

Almost all activities of human life, such as economics, transportation, utilities and education, heavily rely on software systems that have been rapidly becoming larger and lager. No one doubts that such reliance on software systems will be surely becoming lager and larger. Thus, it is inevitable to make software systems more reliable in future. One promising way to do so is to make specifications more reliable because it is known that most flaws are introduced at the upstream phases of software development processes. Use of formal specification languages makes it possible to develop high-quality specifications. Our experiences on formal verification, especially interactive theorem proving, of software systems also suggest that formal specifications can be improved by conducting interactive theorem proving that such specifications enjoy desired properties.

CafeOBJ is a state-of-the-art algebraic specification and verification language, one of few computer languages that has been designed and developed in Japan and used world-wide. CafeOBJ makes it possible to formally specify software designs and verify that such designs enjoy desired properties by writing what are called proof scores in CafeOBJ and executing them with the CafeOBJ system. Specifications and proof scores are expressed in equations and executable by interpreting the equations as left to right rewriting rules. It implies that proof scores are equational programs and formal verification conducted by writing proof scores is more flexible than that done by other existing proof assistants. On the one hand, proof scores are subject to human errors. To overcome this weakness, a proof assistant for CafeOBJ has been recently developed. We will explain how to specify software designs in CafeOBJ, how to verify that such designs enjoy desired properties both by writing proof scores and with the proof assistant for CafeOBJ with some concrete examples, such as natural numbers and simple mutual exclusion protocols.

In cooperation with

  • 1. Hosei University
  • 2. The Institute of Electronics, Information and Communication Engineers (IEICE)
  • 3. Japan Society for Software Science and Technology (JSSST)


  • 1. The Murata Science Foundation