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.

Registration

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
Fees
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
Fees
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
Fees
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
Fees
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
Fee
One extra conference banquet ticket 16,000 JPY


Program

Final Program for ICFEM 2016 Main Conference



Monday, 14 November 2016

09:00 ~ 10:00Registration (4th Floor, Conference Room 4A)
    ・Room: 4A (4th Floor)   FMMDD Workshop
    ・Room: 3D (3rd Floor)   FTSCS Workshop


FMMDD Workshop (4th Floor, Conference Room 4A)

10:00 ~ 10:05 Introduction from the Chairs
10:05 ~ 11:05 Invited talk 1
Stupid Tool Tricks for Smart Model Based Design
Mark Lawford.
11:05 ~ 11:20 Coffee break
11:20 ~ 12:50 Technical talks
ProRef: An Automatic Authentication Protocol Refinement Tool for Extracting Formal Models
Quanqi Ye, Guangdong Bai, Naipeng Dong and Jin Song Dong.

Modeling Requirements for Quantitative Consistency Analysis and Automatic Test Case Generation
Tom Bienmüller, Tino Teige, Andreas Eggers and Matthias Stasch

Tool Support for Model-Based Database Design with Event-B
Ahmed Al-Brashdi, Michael Butler, Abdolbaghi Rezazadeh and Colin Snook
12:50 ~ 13:50 Lunch
13:50 ~ 14:50 Invited talk 2
Assured and Correct Dynamic Update of Controllers
Kenji Tei
14:50 ~ 15:50 Technical talks
PAndA^2: Analyzing Permission Use and Interplay in Android Apps (Tool Paper)
Manuel Toews, Marie-Christine Jakobs and Felix Pauck.

A Formal Approach to Use Case Driven Testing
Rajiv Murali, Andrew Ireland and Gudmund Grov
15:50 ~ 16:20 Coffee break
16:20 ~ 16:50 Invited industrial presentation
A trial application of B method for an embedded device by constructing B model via UM
Daichi Mizuguchi
16:50 ~ 17:40 Technical talk
Safety Kernel for Control Systems Design
Alexei Iliasov
17:40 ~ 17:50 Closing



FTSCS Workshop (3rd Floor, Conference Room 3D)

10:00 ~ 10:10 Opening
10:10 ~ 11:00 Specification and verification
Specification and Verification of Synchronization with Condition Variables
Pedro Gomes, Dilian Gurov and Marieke Huisman

An interval logic for stream-processing functions: A convolution-based construction
Brijesh Dongol
11:00 ~ 11:30 Coffee break
11:30 ~ 12:20 Automotive and railway systems
Automating Time Series Safety Analysis for Automotive Control Systems in STPA using Weighted Partial Max-SMT
Shuichi Sato, Shogo Hattori, Hiroyuki Seki, Yutaka Inamori and Shoji Yuen

Uniform Modeling of Railway Operations
Eduard Kamburjan and Reiner Hähnle
12:20 ~ 13:30 Lunch
13:30 ~ 15:20 Invited talk + Security, Internet of things
On Two Higher-Order Extensions of Model Checking
Invited talk: Naoki Kobayashi

Formal Verification of Gate-Level Multiple Side Channel Parameters to detect Hardware Trojans
Imran Abbasi, Faiq Khalid Lodhi, Awais Kamboh and Osman Hasan

Formal Probabilistic Analysis of a WSN-based Monitoring Framework for IoT Applications
Maissa Elleuch, Osman Hasan, Sofiene Tahar and Mohamed Abid
15:20 ~ 15:50 Coffee break
15:50 ~ 17:05 Cyber-physical systems and parameterized verification
Shared-Variable Concurrency, Continuous Behaviour and Healthiness for Critical Cyberphysical Systems
Richard Banach and Huibiao Zhu

Applying parametric model-checking techniques for reusing real-time critical systems
Baptiste Parquier, Laurent Rioux, Rafik Henia, Romain Soulat, Olivier Roux, Didier Lime and Étienne André

Parameterised Verification of Stabilisation Properties via Conditional Spotlight Abstraction
Nils Timm and Stefan Gruner
17:05 ~ 17:20 Closing



Tuesday, 15 November 2016

09:00 ~ 10:00Registration (4th Floor, Conference Room 4A)
    ・Room: 3D (3rd Floor)   SOFL+MSVL Workshop
    ・Room: 4A (4th Floor)   CafeOBJ Tutorial


SOFL+MSVL Workshop (3rd Floor, Conference Room 3D)

10:00 ~ 10:10 Opening
10:10 ~ 11.00 Invited talk (Chair: Zhenhua Duan)
A CEGAR based Approach to Verifying Web Application
Haikou Miao
11:00 ~ 11:30 Coffee break
11:30 ~ 12:30 Session 1 (Chair: Huaikou Miao)
Formal Development of Linear Structure Reusable Components in PAR Platform
Qimin Hu, Jinyun Xue and Zhen You

The Implementation of MSVL Proof System in Coq
Lin Qian, Zhenhua Duan and Nan Zhang

Orchestration Combinators in Apla+ Language
Zhen You and Jinyun Xue
12:30 ~ 13:30 Lunch
13:30 ~ 15:30 Session 2 (Chair: Jinyun Xue)
Runtime Verification Monitor Construction for Three-valued PPTL
Xiaobing Wang, Dongmiao Liu, Zhenhua Duan and Liang Zhao

Model Checking of a Mobile Robots Perpetual Exploration Algorithm
Ha Thi Thu Doan, François Bonnet and Kazuhiro Ogata

A Case Study of a GUI-Aided Approach to Constructing Formal Specifications
Fumiko Nagoya and Shaoying Liu

On Termination and Boundedness of Nested Updatable Timed Automata with One Updatable Clock
Yuwei Wang and Guoqiang Li

SMT-based Bounded Model Checking for Cooperative Software with a Deterministic Scheduler
Haitao Zhang and Yonggang Lu

An Automated Solving Procedure for String Function Constraints
Xuzhou Zhang, Ying Xing, Yunzhan Gong, Yawen Wang, Rongyu Liang and Honghui Li.
15:30 ~ 15:55 Coffee break
15:55 ~ 17:55 Session 3 (Chair: Xiaobing Wang)
Instant-based & State-based Analysis of Infinite Logical Clock
Qingguo Xu, Robert De Simone and Julien Deantoni.

Applying SOFL to a Railway Interlocking System in Industry
Juan Luo, Shaoying Liu, Yanqin Wang and Tingliang Zhou

A Visual Modeling Language for MSVL
Xinfeng Shu, Chao Li, and Chang Liu

E-SSL:An SSL Security-Enhanced Method for Bypassing MITM Attacks in Mobile Internet
Ren Zhao, Xiaohong Li, Guangquan Xu, Zhiyong Feng and Jianye Hao

Automated safety analysis on scenario-based requirements for train control system
Xi Wang

Reliability Testing Data Generation: A Weighted Parameter and Combination Method
Dalin Zhang, Yunzhan Gong, Jianwei Sui and Haitao Zhang
17:55 ~ 18:00 Closing



CafeOBJ Tutorial (4th Floor, Conference Room 4A)

Lecturers: Kokichi Futatsugi and Kazuhiro Ogata, JAIST

Overview:
CafeOBJ is one of the most advanced algebraic formal specification language systems with a rewriting/reduction engine that can be used for interactive verification. Proof scores are scripts for verification and provide versatile ways to prove properties of specifications. The tutorial gives foundations and techniques of CafeOBJ/ProofScores by using elementary examples of natural numbers, sequences, sets and a simple mutual exclusion protocol.
10:00 ~ 11:00 Proof Scores on Peano Style Natural Numbers
11:00 ~ 11:15 Coffee break
11:15 ~ 12:15 Modeling, Specification, and Simulation of Mutual Exclusion Protocol QLOCK
12:15 ~ 14:00 Lunch
14:00 ~ 15:00 Proof Score Development for QLOCK with Specification Calculus
15:00 ~ 15:30 Coffee break
15:30 ~ 16:30 Formal Verification of Observational Transition Systems with Proof Scores
16:40 ~ 17:40 Formal Verification of Observational Transition Systems with CafeOBJ CITP



Wednesday, 16 November 2016

08:30 ~ 09:00 Registration (8th Floor, Banquet Room C)
09:00 ~ 09:15 Main Conference Opening (8th Floor, Banquet Room B)
09:15 ~ 10:15 Keynote speech (Chair: Shaoying Liu)
Combinatorial Testing and Its Applications
W. Eric Wong
10:15 ~ 10:45 Coffee break
10:45 ~ 12:15 Testing/Symbolic Execution (Chair: Sungdeok Cha)
Automated Requirements Validation for ATP Software via Specification Review and Testing
Weikai Miao, Geguang Pu, Yinbo Yao, Ting Su, Danzhu Bao and Yang Liu

Automatic Instance Generation for Validating Alloy Models
Takaya Saeki, Fuyuki Ishikawa and Shinichi Honiden

A General Lattice Model for Merging Symbolic Execution Branches
Dominic Scheurer, Reiner Hähnle and Richard Bubel
12:15 ~ 14:00 Lunch
14:00 ~ 16:00 Hybrid/Service-Based Systems (Chair: Elena Troubitsyna)
A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata
Ryo Yanase, Tatsunori Sakai, Makoto Sakai and Satoshi Yamane

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

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

Service Adaptation with Probabilistic Partial Models
Manman Chen, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun and Jin Song Dong
16:00 ~16:30 Coffee break
16:30 ~ 18:00 Security (Chair: Fatiha Zaidi)
A Formal Approach to Identifying Security Vulnerabilities in Telecommunication Networks
Linas Laibinis, Elena Troubitsyna, Inna Pereverzeva, Ian Oliver and Silke Holtmanns

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

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

Thursday, 17 November 2016

09:00 ~ 10:00 Keynote speech (Chair: Mark Lawford) (8th Floor, Banquet Room B)
A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case
Tom Maibaum
10:00 ~ 10:30 Coffee break
10:30 ~ 12:30 Formal Verification (Chair: Toshiaki Aoki)
Towards the formal verification of data-intensive applications through metric temporal logic
Francesco Marconi, Marcello M. Bersani, Madalina Erascu and Matteo Rossi

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

Formal Availability Analysis using Theorem Proving
Waqar Ahmed and Osman Hasan

Formal Verification of the rank Algorithm for Succinct Data Structures
Akira Tanaka, Reynald Affeldt and Jacques Garrigue
12:30 ~ 14:00 Lunch
14:00 ~ 16:00 Concurrency/Distributed Systems (Chair: Jin Song Dong)
Contextual trace refinement for concurrent objects: Safety and progress
Brijesh Dongol and Lindsay Groves

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

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

An Event-B development process for the distributed BIP framework
Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix and Mamoun Filali-Amine
16:00 ~ 16:20 Coffee break
16:20 ~ 17:20 Panel Discussion (Chair: Shaoying Liu)
How can formal methods become effective and acceptable “medicine” for software engineering “diseases”?
Panellists: Kokichi Futatsugi, Tom Maibaum, Jin Song Dong, Sungdeok Cha
17:30 ~ 21:30 Banquet (Symphony Tokyo Bay Dinner Cruise)

Friday, 18 November 2016

09:00 ~ 10:00 Keynote speech (Chair: Kazuhiro Ogata) (8th Floor, Banquet Room B)
Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa's Case
Keijiro Araki
10:00 ~ 10:30 Coffee break
10:30 ~ 12:30 Model Checking (Chair: Cong Tian)
Partial Order Reduction for State/Event Systems
Shuanglong Kan

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

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

Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots
Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Félix Ingrand and Anthony Mallet
12:30 ~ 14:00 Lunch
14:00 ~ 15:30 Real-Time Systems (Chair: Richard Banach)
Decision Problems for Parametric Timed Automata
Étienne André, Didier Lime and Olivier H. Roux

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

An SMT-based Approach to the Formal Analysis of MARTE/CCSL
Min Zhang, Frederic Mallet and Huibiao Zhu
15:30 ~ 16:00 Coffee break
16:00 ~ 17:00 Formal Analysis (Chair: Shin Nakajima)
Checking SysML Models for Co-Simulation
Nuno Amalio, Richard Payne, Ana Cavalcanti and Jim Woodcock

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

Click here to download pdf file of the program.

Proceedings

Formal Methods and Software Engineering

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



The digital version of ICFEM 2016 proceedings, LNCS 10009

Hotels

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
http://www.ghi.gr.jp/en/accommodation/

・Arkadia Ichigaya
http://www.arcadia-jp.org/top.htm

・APA Hotel Tokyo-Kudanshita
http://www.apahotel.com.e.ju.hp.transer.com/language/shutoken/21_tokyo-kudanshita.html

・Hotel Monterey Hanzomon
http://www.hotelmonterey.co.jp/en/htl/hanzomon/index.html

・Hotel metropolitan Edmont
http://www.edmont.jp

・Tokyo Dome Hotel
http://www.tokyodome-hotels.co.jp/e/

・Flexstay Inn Iidabashi
https://www.mystays.com/en/hotel/Flexstay-Inn-Iidabashi?_ga=1.54935651.978011498.1468450528

Venue

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
Tell:+81-3-5227-6911

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)

Title:


Combinatorial Testing and Its Applications

Abstract:


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).

Bio:


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)

Title:


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

Abstract:


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.

Bio:


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)

Title:


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

Abstract:


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

Workshop/Tutorial

Workshops:


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

Tutorial:


AbbreviationDay(s)
CafeOBJNovember 15, 2016 (one day)

SOFL+MSVL

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

Details+

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

Submission:


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

FTSCS

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 >

FM&MMD

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 >

Tutorial:CafeOBJ

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.


See the tutorial website for more details >

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)

Co-Sponsorships

  • 1. The Telecommunications Advancement Foundation (TAF)
  • 2. The Murata Science Foundation
  • 3. Kayamori Foundation of Informational Science Advancement