Ingo Sander – KTH Royal Institute of Technology, Stockholm, Sweden

System Design with ForSyDe

Current industrial design flows do not have a clear path from the functional specification to the final implementation and cannot provide real-time guarantees. The ForSyDe methodology addresses this challenge by combining formal models based on the theory of models of computation (MoCs) with the functional programming paradigm and time-predictable computation platforms, envisioning a correct-by-construction design flow that can provide real-time guarantees. The lecture will cover the underlying ideas of ForSyDe, the current state of the methodology, and available modelling and tool support.

Bio: Ingo Sander holds a position as professor in Electronic Systems Design at KTH Royal Institute of Technology, Stockholm, Sweden. His main research interests are located in the area of design methodologies for embedded systems including system modeling, design space exploration and system synthesis.

Hokeun Kim – Arizona State University, USA

Introduction to Lingua Franca, a polyglot coordination language and runtime for time-sensitive reactive systems

Lingua Franca (LF) is a polyglot coordination language built to enrich mainstream target programming languages (currently C, C++, Python, TypeScript, and Rust) with deterministic reactive concurrency and the ability to specify timed behavior. LF is supported by a runtime system that is capable of concurrent and distributed execution of reactive programs that are deployable on the Cloud, the Edge, and even on bare-iron embedded platforms. A Lingua Franca program specifies the interactions between components called reactors. The logic of each reactor is written in plain target code. A code generator synthesizes one or more programs in the target language, which are then compiled using standard toolchains. If the application has exploitable parallelism, then it executes transparently on multiple cores without compromising determinacy. A distributed application translates into multiple programs and scripts to launch those programs on distributed machines. The communication fabric connecting components is synthesized as part of the programs.

Bio: Hokeun Kim is an assistant professor of Computer Science and Engineering (CSE) in the School of Computing and Augmented Intelligence (SCAI) at Arizona State University (ASU). Before joining ASU, he was an assistant professor in the Dept. of Electronic Engineering at Hanyang University, Seoul, Korea, and an assistant researcher in the Dept. of EECS at UC Berkeley. He received his Ph.D. degree in EECS from UC Berkeley in 2017 with a focus on IoT security. After graduating from Berkeley, he spent four years in industry in Silicon Valley and continued research on the Internet and cloud security at Google before returning to academia in 2021. His research interests include computer security, the IoT, real-time systems, cyber-physical systems, and computer architecture. He received the ACM/IEEE Best Paper Award and IEEE Micro Top Picks Honorable Mention for his research contributions to IoT and computer architecture research.

Michele Lora and Sebastiano Gaiardelli - University of Verona, Italy

SysML v2 and its Applications in the Manufacturing Domain

The recent iteration of the SysML standard, i.e., SysML v2, revolutionized most of the concepts of its predecessor SysML 1. The language is no longer based on UML, while it shift its focus from graphical to textual representations. Such choice enabled stricter semantics, and reduced language ambiguities. Thus, making SysML v2 more suitable for structured and rigorous model-based design flows.
This lecture presents the main principles of SysML v2, showing its main features and highlighting the advantages provided by the new standard. Then, the lecture showcases a series of applications of SysML v2 in modeling and designing manufacturing systems and processes.

Bio: Michele Lora is a Assistant Professor at the University of Verona; his research focuses on modeling, simulation, and verification of cyber-physical systems. He is involved as a co-founder and scientific advisor for FACTORYAL S.r.l., a startup specializing in factory automation software that originated as a spin-off from the University of Verona. From 2020 to 2023, he held a Marie Skłodowska-Curie Global Fellowship with dual appointments at the University of Verona and the University of Southern California. Previously he held different research positions in Sweden, the United States and Singapore.

Sebastiano Gaiardelli is a Ph.D. Candidate at the University of Verona. He received the master’s degree in computer science and engineering from the University of Verona in 2021. His research interests include the development of new methodologies for the optimization, reconfiguration, and verification of cyber–physical production systems. He is involved as a co-founder and scientific advisor for FACTORYAL S.r.l., a startup specializing in factory automation software that originated as a spin-off from the University of Verona.

Pierluigi Nuzzo - University of California, Berkeley, USA

Contract-based design for Cyber-Physical Systems with CHASE

The lecture will focus on assume-guarantee contracts, a rich modeling and specification formalism allowing to specify the different aspects and components of a cyber-physical system. The lecture will present the main features of the formalism, the algebra defining the main operations on contracts, and some interesting research results. Then, we will concretely use assume-guarantee by introducing CHASE: a contract-based framework for the heterogeneous analysis and system exploration of cyber-physical systems. During the demonstration, we will see how CHASE can be used to deal with architectural and timing requirements, as well as stochastic specifications.

Bio: Pierluigi Nuzzo is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at UC Berkeley. Before joining UC Berkeley, he was the Kenneth C. Dahlberg Chair and an Associate Professor of Electrical and Computer Engineering and Computer Science at the University of Southern California. He received a PhD degree from UC Berkeley, and BS and MS degrees from the University of Pisa and the Sant’Anna School of Advanced Studies in Pisa. He also held research positions at the University of Pisa and IMEC, Leuven, Belgium, working on mixed-signal integrated circuit design. His current interests focus on computer-aided design and verification methods for safe and dependable autonomous systems, automated generation of assurance cases for system certification, and analysis and design of secure and trustworthy hardware platforms. His awards include the IEEE Council on Electronic Design Automation (CEDA) Ernest S. Kuh Early Career Award, the Okawa Research Grant, the IEEE Technical Committee on Cyber-Physical Systems Early-Career Award, the DARPA Young Faculty Award, the NSF CAREER Award, the UC Berkeley EECS David J. Sakrison Memorial Prize, and several best paper and design competition awards.

Prof. Dr. Klaus Schneider, RPTU Kaiserslautern-Landau, Germany

Using Synchronous Models for the Design of Safety-Critical Embedded Systems

To meet the required real-time constraints, modern embedded systems have to perform many tasks in parallel and therefore require the modeling of concurrent systems with an adequate notion of time. To this end, several models of computation (MoCs) have been defined that specify why (causality), when (time), and which atomic action of the system is executed. The most important classes of MoCs are event-triggered, time/clock-triggered, and data-driven MoCs, each of which has its own advantages and disadvantages. This talk gives an overview of the design flow used in the Averest system developed at the University of Kaiserslautern. The core of this design flow is a synchronous (clock-driven) modeling language called Quartz, which is used for modeling, simulation and formal verification. The use of a synchronous MoC offers many advantages for the early design phases, since formal methods can be easily applied and repeated simulation runs show reproducible results. For synthesis, however, it is difficult to implement the synchronous model for some target architectures, so transformations are used to translate the original models into asynchronous implementations with the same stream-based behavior. Special transformations allow developers to desynchronize the system into asynchronous components in order to synthesize distributed/multithreaded systems from verified synchronous models. The talk also presents the extension of the synchronous language to model hybrid systems, i.e., systems that contain a combination of discrete and analog behavior.

Bio: Klaus Schneider studied Computer Science at the University of Karlsruhe, Germany (now KIT) from 1987-1992 and worked as a researcher at the Institute for Computer Design and Fault Tolerance at the same university from 1992-2001. He then became a full professor at the University of Kaiserslautern, now University of Kaiserslautern-Landau (RPTU). Since then, he has been a member of the faculty, dean, vice dean, and a member of the university senate. He has organized many conferences, including MEMOCODE, ICCD, and FDL, and is a member of many program committees.