Marcel Christian Werner

dblp:309/3405 · DBLP profile ↗
← Back
3ranked-venue papers
3as first author
3since 2021 · last 2023
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 3 · 3 first-author · 3 since 2021Theory of computation · 1 · 1 first-author · 1 since 2021
YearPublicationVenuePosition
2023 Formal Methods-Based Optimization of Dataflow Models with Translation to Synchronous Models
abstract
Graphical dataflow models are widely used for industrial control system implementation and are accepted by users with different backgrounds due to their intuitive visualization of the dataflow. As real-world applications have evolved, the complexity of these diagrams has increased, posing a challenge in the verification and maintenance of software models. In this paper, we argue that the perceived complexity of real-world applications can be simplified and transformed into formal models for reuse in software engineering or formal verification. To overcome the limitations of previous research on optimizing graphical dataflow models in an industrial context, we identify potentially optimizable submodels and optimize them, leaving the non-modifiable components unchanged. The optimized software model is then reconstructed and optionally translated into formal models for reuse or verification purposes. The paper describes the identification of submodels in real-world applications and demonstrates the need for configurability of the optimization. We present an open-source-based implementation using graphical dataflow models of programmable logic controllers and demonstrate the impact of our optimization approach using real-world applications from the literature and vendor-provided examples. The results help to reduce the complexity of existing dataflow models and to reuse existing real-world applications as formal software models.
Marcel Christian Werner, Klaus Schneider 0001
FDL1
2022 From IEC 61131-3 Function Block Diagrams to Sequentially Constructive Statecharts
abstract
Function Block Diagrams (FBDs) are widely used for implementing the software of IEC 61131-3 based systems. In general, there is a risk that FBDs used in industry will become more and more complex during their life cycle, while at the same time strict specifications have to be met. On the other hand, a trend towards model-based design with standardized modeling tools can be observed in software engineering. While previous research focuses on translating existing FBDs to formal models for verification purposes, this paper presents two translations from existing FBDs to sequentially constructive statecharts, thus enabling an intuitive functional reuse for a model-based design. Besides a basic translation in the first approach, it is shown in the second approach that it is possible to improve the readability through code refactoring within the synchronous paradigm.
Marcel Christian Werner, Klaus Schneider 0001
FDL1
2021 Translation of continuous function charts to imperative synchronous quartz programs
abstract
Programmable logic controllers operating in a sequential execution scheme are widely used for various applications in industrial environments with real-time requirements. The graphical programming languages described in the third part of IEC 61131 are often intended to perform open and closed loop control tasks. Continuous Function Charts (CFCs) represent an additional language accepted in practice which can be interpreted as an extension of IEC 61131-3 Function Block Diagrams. Those charts allow more flexible positioning and interconnection of function blocks, but can quickly become difficult to manage. Furthermore, the sequential execution order forces a sequential processing of possible independent and thus possibly parallel program paths. The question arises whether a translation of existing CFCs to synchronous programs considering independent actions can lead to a more manageable software model. While current formalization approaches for CFCs primarily focus on verification, the focus of this approach is on restructuring and possible reuse in engineering. This paper introduces a possible automated translation of CFCs to imperative synchronous Quartz programs and outlines the potential for reducing the states of equivalent extended finite state machines through restructuring.
Marcel Christian Werner, Klaus Schneider 0001
MEMOCODE1