Frontiers of Computer Science (FCS), 2016

Formal methods are showing an increasingly important role in embedded system design. Several architectural modelling languages for embedded systems have emerged in recent years, including the SAE AADL, or SysML, and the MARTE profile for UML. We try to introduce the latest research in the following series of special issue from a broader perspective.
This issue will focus on semantic of modelling embedded architectures. It will bring together research interested in defining precise semantics of an architecture description language and using it for building tools that generate analytical models from architectural ones. Despite recent research activity in this area to use semantic interpretation of architectural models for analytical model generation, we observe a significant gap between current state of the art and the practical need to handle complex models. In practice, most approaches cover a limited subset of the language and target a small number of modelling patterns. A more general approach would most likely require an interpretation of the semantics of the language by the tool, instead of hard-coding the semantics and patterns into the model generator. The definition of a design flow suitable for the use of architecture modelling languages in critical system design demands implementation of formal methods to analyse, verify, compose and integrate heterogeneous software and hardware components with the physical environment: a formal, cyber-physical, perspective.
The aim of this special issue is to share expertise and jointly contribute to key scientific topics in the aim of developing a standardised contract-based design environment for embedded architecture design that is based on formal methods to reliably assist system architects in integrating cyber-physical systems from heterogeneous components.

We invite previously unpublished articles on topics listed below (not an exhaustive list):
● How to support modelling in the large, in different dimensions? An architectural description should tie together system requirements, platform requirements and highlight trade-offs, etc. How to formalise these requirements and to assess them with respect to real-time?
● How to provide a better description of the semantics for an architecture description language in a way that is both easier to understand by humans and easier to interpret by a tool? Thus user-friendly semantics should be soundly linked with existing verification tools. We also envision enhancing the model with the certification credits provided by the validation.
● How to handle extension of the semantics to address new demanding architectures like multi-core, new network technologies, and their application to large-scale systems?
● How to model complex architectural frameworks, such as synchronous or time-triggered designs, RAVENSCAR-compliant systems, multiple independent levels of security (MILS), or integrated modular avionics (IMA)?
● How to interconnect the architecture modelling of software-intensive embedded systems to physical concerns like energy consumption, electro-magnetic compatibility?

Authors can submit their manuscripts via the Manuscript Tracking System at
http://mc.manuscriptcentral.com/hepfcs

Provisional timeline for submission, review, and publication:

● July 1st 2016          Deadline for submissions
● October 1st 2016     Response to authors
● October 15th          Deadline for revision
● November 1st         Final review result
● November 15th       Final submission due

Guest Editors

Jean-Pierre Talpin, INRIA, France, Jean-Pierre.Talpin@inria.fr
Kai Hu, Behang University,China,  hukai@buaa.edu.cn