First International Workshop on Knowledge and MOdel-driven engineering in formal development of Trustworthy Systems.

Co-located with TASE 2019 (13th International Symposium on Theoretical Aspects of Software Engineering),  29 July – 1 August 2019, Guilin, China

Extended deadline: 8 June 2019

New: Selected papers will be invited after the workshop to submit an extended version to the Journal of Computer Languages

Development of trustworthy systems constitutes one of the major engineering challenges. Both functional correctness and non-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 on 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.

Though the benefits of using both formal and model-driven techniques in the design of trustworthy systems are widely acknowledged, several challenges remain open.

In particular, there are ongoing debates about achieving a balance between flexibility and rigor in integrated modelling, analyzing the interplay between functional and non-functional properties, 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.

Another challenge concerns the modelling and handling of domain knowledge in formal models and formal developments. Indeed, systems are generally associated to information issued from the application domain in which these systems evolve. However most of the formal methods based on proof systems rely on the definition and use of basic theories in which domain knowledge is difficult to capture. Generally, the formalisation of this kind of knowledge is either omitted or hardcoded in the formal model. For example, though units of measurement of different parameters are critical for correctness of calculations typically they are not explicitly documented in the model and only kept in mind of the model designer. Therefore, they are not shared in the same way as for basic theories that can be reused in several formal developments. Furthermore, making explicit domain knowledge in formal models can facilitate the formal specification of new properties. On the other hand, ontologies are formal models describing the meaning of concepts of a domain and ontology languages are most often supported by efficient reasoning tools that could help designers for discharging proofs in formal developments.

The aims of this workshop are:

  • to advance the understanding in the area of developing and applying formal and model-driven techniques that integrate domain knowledge 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.

The topics of interest include, but are not limited to:

  • Formal methods in model-driven development
  • Knowledge- and model-driven development for formal methods
  • Quality assurance for models and model transformation
  • Model transformation and refinement
  • Integrated analysis of functional and non-functional properties of trustworthy systems
  • Methods and tools integrating knowledge based, graphical and formal approaches
  • Domain-specific formal and model-driven approaches
  • Handling of knowledge models, like ontologies, in formal system developments
  • Formal modelling languages and techniques to model domain knowledge
  • Case studies that illustrate the need to handle domain knowledge