Accepted Papers

We have finished the reviewing process for the CSMML workshop.

In total, we received 15 submissions of which 12 resulted in full submissions.

Each paper was reviewed by at least 2 Program Committee members, and the decision was overseen by the Program Chairs.

Following an online discussion, we decided to accept 2 full papers and 2 short papers, with an acceptance rate of 33.3%.

List of accepted papers with their abstracts:

Time insertion functions as a tool to guarantee security of processes with respect to timing attacks are discussed and studied. We work with a security property called opacity and we investigate how it can be enforced by such functions.

The time insertion function can alter time behaviour of original system by inserting some time delays to guarantee its security. We investigate conditions under which such functions do exist and also some of their properties.

Eugeny Semenov, Sheng Kai, Chen Gen, Dmitry Luciv and Dmitry Koznov. Domain Specific Modeling Language for Device Management in Telecommunication Product Line

In the present paper, we consider the task of creating hardware specifications for telecommunication devices that close the communication gap between hardware engineers and software developers. This task has arisen during the development of a family of telecommunication systems at Huawei. The specifications need to describe hardware from the viewpoint of driver development (i.e., device management), omitting many hardware details and including information for automatic generation of driver data structures and signatures. Furthermore, they need to be comprehensive and illustrative for both engineering groups. To meet this challenge, we propose a visual language based on the domain-specific modeling approach (DSM). The language supports five view types (representations): Structured view (all structural elements of a device), Composite view (all connections of a device), Datapath view (device parts that process the data flow), Control view (device parts that control the data flow processing), and Service view (device parts that provide additional functionality). We present an implementation of the language built with the Eclipse Modeling Toolset xtext/EMF/Sirius and integrated into a development environment for device management. We have received positive feedback from the driver developers.

In this paper, we propose an approach to checking consistency of control software requirements described using pattern-based notation. This approach can be used at the beginning of control software verification to effectively identify contradicting and incompatible requirements. In this framework, we use pattern-based Event-Driven Temporal Logic (EDTL) to formalize the requirements. A set of requirements is represented as a set of EDTL-patterns which formal semantics defined by formulas of linear-time temporal logic LTL. Based on this semantics, we define the notion of requirement inconsistency and describe restrictions on the values of pattern attributes which make requirements inconsistent. Checking algorithm takes as an input pairs of requirements and compare their attributes. Its output is sets of consistent, inconsistent and incomparable requirements.

This paper deals with leveraging the IEC 61499 Function Blocks with the poST language. The poST language is a process-oriented extension of the IEC 61131-3 Structured Text (ST) language. The language targets specifying stateful behavior of PLC-based control software. The main purpose of our contribution is to provide coherence of the PLC source code with technological description of the plant operating procedure. The language combines the advantages of FSM-based programming with conventional syntax of the ST language and can be easily adopted by the community. The poST language assumes that a poST-program is a set of weakly connected concurrent processes. Each process is specified by a sequential set of states. The states are specified by a set of the ST constructs, extended by TIMEOUT operation, SET STATE operation, and START / STOP / check state operations to communicate with other processes. The paper describes the basics of the poST language, design constructs, and demonstrates usage of the poST language by developing control software for a wheel-chair elevator, and discusses the poST language over the control software implementation in Execution Control Chart.