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.

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


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 Submitted manuscripts must be written in English and should be no longer than 20 pages in Springer’s LNCS format described at 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.

Authors of selected papers from SOFL+MSVL 2017 will be invited to submit an extended version to a special section of IEEE Transactions on Reliability (T-Rel). However, such an invitation does not imply acceptance of the paper. All the submissions will be evaluated following the guidelines set by T-Rel. Only those which satisfy all the criteria will be accepted for publication.

Important dates

  • Paper submission
  • (31 July 2017) 16 Aug 2017
  • Acceptance/Rejection notification
  • (2 September 2017) 18 September 2017
  • Workshop
  • 16 November 2017
  • Camera ready Paper Due
  • 22 December 2017

    Conference Organizing Committee

    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
    • Richard Lai, La Trobe University, Australia
    • Karl Leung, Hong Kong Institute of Vocational Education
    • Guoqiang Li, Shanghai Jiaotong University, China
    • Shaoying Liu, Hosei University, Japan
    • Huaikou Miao, Shanghai University, China
    • 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
    • Xinfeng Shu, Xi'an University of Posts and Telecommunications, China
    • Jing Sun, University of Auckland, New Zealand
    • Cong Tian, Xidian University, China
    • Xi Wang, Shanghai University, China
    • Xiaobing Wang, Xidian University, China
    • Haitao Zhang, Lan Zhou University, China
    • Hong Zhu, Oxford Brookes University, UK

    Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD)

    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 ongoing debates about achieving a balance between flexibility and rigor in integrated modelling, analyzing the interplay between functional and extra-functional properties, using domain-specific frameworks as well as addressing trustworthiness at different architectural levels.

    Moreover, the development of systems is becoming more and more incremental and practices like continuous integration and deployment are the ambition of many companies including those working with safety-critical systems. This implies that formal and model-driven techniques should support incremental verification thus enabling the continuous addition of new features while ensuring system trustworthiness.

    The aims of this workshop are:
    - to advance the understanding in the area of developing and applying formal and model-driven techniques for designing trustworthy systems
    - to discuss the emerging issues in the area
    - to improve the dialog between different research communities and between academia and industry
    - to discuss a roadmap of the future research in the area
    - to create a forum for discussing and disseminating the new ideas and the research results in the area

    We welcome new ideas, even though not completely validated, as well as experiences and lessons learned of using existing techniques in industry or in large open source projects.

    Topic areas

    The topics of interest include, but are not limited to:
    1. Formal methods in model-driven development
    2. Model-driven development for formal methods
    3. Quality assurance for models and model transformation
    4. Model transformation for formal models
    5. Model transformation and refinement
    6. Formal and model driven approaches to engineering safety- critical, fault-tolerant and secure systems
    7. Integrated analysis of functional and extra-functional properties of trustworthy software-intensive systems
    8. Methods and tools integrating graphical and formal approaches
    9. Lightweight formal methods for dependability and security
    10. Formal and model-driven engineering of trustworthy cyber-physical systems
    11. Domain-specific formal and model-driven approaches

    Submission Types

    All submissions must be original, unpublished, and cannot be simultaneously submitted for publication elsewhere. Papers of the following types are solicited:

  • Research papers focusing on advanced and novel theories, methodologies, or mechanisms
  • Tool papers focusing on useful and practical tools, their integration and interoperability
  • Experience papers with a focus on deployment, evaluation and lessons learned

  • Submissions must consist of no more than 10 pages for Research papers and 6 pages for Tool/Experience papers (including all the materials) in the LNCS format.

    Important dates

  • Paper submission:
  • 10 September 2017
  • Notification:
  • 9 October 2017

    The workshop page:

    First International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development

    Background and Objectives

    Most of methods based on proof systems, such as theorem provers, model checkers or any reasoning systems, rely on the definition and use of basic theories (logic, algebraic, types, etc.) in order to support the expression of proofs in formal developments. They also propose mechanisms and operators to define new theories (inside contexts or theories or species, like in Event-B, COQ, Isabelle/HOL, FOCAL, Nuprl, ASM, PVS, etc.) or to enrich their basic theories. In general, the definition of a theory is based on mathematical and logical abstract concepts that support the formalisation of the studied hardware and/or software systems. In other words, the semantics of such formalised systems is expressed in this theory; i.e. the used theory gives the semantics of all the systems formalised in this theory and the required properties of these systems are expressed and checked in the same theory. This kind of semantics represents the implicit semantics. Note that the same semantics is used for a wide variety of heterogeneous hardware and/or software systems.

    Generally, hardware and/or software systems are associated to information issued from the application domain in which they evolve. For example, one integer variable (typed by an integer in the theory) may denote a temperature expressed in Celsius degrees, whilst another one may denote a pressure measured in bars at the extreme limit of the left wing of an aircraft in the landing phase. In general, this kind of knowledge is omitted by the produced formalisations or their formalisation is hardcoded in the designed formal model. If this knowledge carried by the concepts manipulated in these formal models is still in the mind of the model designer, it is not explicitly formalised and therefore, it is not shared in the same way as for implicit theories that can be reused in several formal developments. This kind of knowledge represents the explicit semantics.

    The objective of the meeting is to discuss on mechanisms for reducing heterogeneity of models induced by the absence of explicit semantics expression in the formal techniques used to specify these models. More precisely, the meeting targets to highlight the advances in handling both implicit and explicit semantics in formal system developments.

    Topic areas

    Discussions, presentations and more generally, contributions shall address one or more topics described below
    1. Show that when making explicit the domain knowledge in formal models, several relevant hidden (because they are not explicitly modelled in classical formal modelling languages) properties can be handled
    2. How knowledge models, like ontologies, can be handled in formal system developments?
    3. What are the candidate formal modelling languages and techniques to model such domain knowledge? What are the reasoning capabilities entailed by these modelling languages?
    4. Define relevant case studies that illustrate the need to make explicit domain properties?
    5. Define composition mechanisms to handle domain knowledge in formal modelling techniques.
    Beyond the technical results targeted by the proposed meeting, social, economic and resilience impacts are expected. These impacts are built on the foundations of heterogeneity reduction and formal model alignment.


    Submissions to the workshop 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 workshop. The proceedings are planned to be published in EPTCS (to be confirmed).

    Papers should be written in English and not exceed 15 pages in EPTCS format ( for details). Submission should be made through the IMPEX 2017 submission page ( conf=impex2017), handled by the EasyChair conference management system.

    Authors of selected papers from IMPEX 2017 will be invited to submit an extended version for the journal ISSE Springer . However, such an invitation does not imply acceptance of the paper. All the submissions will be evaluated following the guidelines set by the journal. Only those which satisfy all the criteria will be accepted for publication.

    Important dates

  • Abstract Submissions(optional):
  • 18 September 2017
  • Full Paper Submissions:
  • 23 September 2017
  • Acceptance/Rejection Notification:
  • 8 October 2017
  • Camera-ready Papers for preliminary proceedings:
  • 28 October 2017
  • Camera-ready Papers for post-proceedings:
  • 30 November 2017

    The workshop page:

    11th NSFC-JSPS Joint Workshop on Formal Methods (NSFC-JSPS FM 2017)