Forum on specification & Design Languages



Summer School Program


Monday 11/09 Tuesday 12/09 Wednesday 13/09 Thursday 14/09 Friday 15/09
08:00 Welcome Registration
08:30 Opening Remarks Guest Lecture 4: Michele Lora
09:00 The Industrial Computer Engineering (ICE) Laboratory
Franco Fummi
Network aspects in OPERA 4.0 – D. Quaglia Guest Lecture 1: F. Oppenheimer Guest Lecture 3: David Broman
10:00 Tutorial 3: CHASE
10:30 Coffee Break Coffee Break Coffee Break Coffee Break
11:00 Modeling Cyber Physical Production Systems – M. Lora Demonstration of the ICE Laboratory – D. S. Cheng Tutorial 1: Waveforms Tutorial 2: CAT language Coffee Break
11:30 Final Exam
12:00 Keynote 1: Infineon Keynote 2: Robert Wille,
Design for Quantum Computing:
New Paradigms, new methods, new tools?
12:30 Lunch Lunch
13:00 Lunch Lunch Lunch
13:30 Nonlinear Model Predictive Control tools for real-time applications Control – A. Beghi Transfer to Turin
14:00 Guest Lecture 2: M. Mendler Panel Session: The Impact of AI
to the Future of Design and
specification Languages
Closing Remarks & Best Paper Award
15:00 Coffee break
15:30 Modeling cybersecurity for industrial CPS – M. Rocchetto Coffee Break
16:00 Project Dissemination
17:00 Ph.D Forum
18:30 Welcome Reception
19:00 Moving to dinner
19:30 Dinner

Guest Lectures Speakers

Franco Fummi – University of Verona, Italy

September 11 (9:00 – 10:30) – The Industrial Computer Engineering (ICE) Laboratory

The ICE Laboratory was set up to promote synergy between the technological innovation of Industry 4.0 and the education and research centers located in the Verona area. The ICE Laboratory is divided into several technological areas, each representing a type of production. A logistics system consisting of an AGV transport line connects the different areas, thanks to an innovative software stack for control and monitoring. The lecture will present the five-year experience of setting up a laboratory for advanced manufacturing, focusing on the laboratory architecture, its technologies and the results obtained by relying on such a complex case study.

Bio: Franco Fummi received the Laurea degree in Electronic Engineering at Politecnico di Milano in 1990 and the Ph.D.in Electronic and Communication Engineering in 1994 at Politecnico di Milano. In 1993 he was Research Assistant at the department of Computer Science of the University of Victoria (B.C.). In 1996 he obtained the position of Assistant Professor in Computer Science at the Dipartimento di Elettronica e Informazione of Politecnico di Milano where he remained until October 1998.
In July 1998 he obtained the position of Associate Professor in Computer Architecture at the Computer Science Department of Università di Verona. Since March 2001 he is Full Professor in Computer Architecture at Università di Verona, before at the Computer Science Department and then at the Department of Engineering IM (DIMI). He is leading Cyber-physical and IoT Systems Design (CISD) group of the Università di Verona, currently composed of more than 20 people and working on hardware description languages and electronic design automation methodologies for modeling, verification, testing and optimization of cyber-physical systems. Since 2018 he is the project manager of the Industrial Computer Engineering (ICE) Laboratory at the University of Verona: a facility serving as a technological demonstrator and research laboratory, functional to rethink industrial processes such as additive and subtractive manufacturing, quality control, assembly, and parts storage.
He is also a co-founder of two spin-off companies: EDALab, focused on networked embedded systems design; and the automation control software company FACTORYAL.

Michele Lora – University of Verona, Italy

September 11 (11:00 – 12:30) - Modeling Cyber Physical Production Systems

Model Based Software Engineering (MBSE) techniques allows encapsulating and abstracting into models systems architectures and functionalities. Models are able to capture widely heterogeneous components, dynamics and behaviors as well as a large variety of different viewpoints. Thus, the MBSE approach is particularly well suited to design advanced manufacturing systems. Indeed, supporting MBSE when designing production systems will require to have languages and specification methods powerful enough to capture today’s manufacturing requirements and systems’ specifications. This lecture presents the languages currently used for the specification of manufacturing systems, such as AutomationML and BPMN. The presentation will highlights the limitations of such languages when dealing with more advanced cyber-physical production systems. Then, it will present some strategies to mitigate such limitations exploiting more advanced languages such as SysML. Finally, it will introduce the features of the upcoming new version of SysML, namely SysML v2, while showing how the new features are better suited to specify advanced manufacturing systems.

September 15 (08:30 – 10:00) - CHASE: Contract-based Heterogeneous Analysis and Systems Exploration

The DeFacto (Design Automation for Smart Factories) project aims at advancing the field of cyber physical systems design and its automation by developing modeling paradigms, scalable algorithms, and tools to aid the design of smart manufacturing systems, ultimately fostering their widespread adoption. Central to the project is the CHASE framework, combining specification and modeling features with rigorous synthesis and verification relying on Assume/Guarantee (A/G) Contracts. The front-ends of CHASE support automatic translation of requirements into low-level mathematical languages. The synthesis, analysis, and verification back-ends use the mathematical formalism of contracts to reason about the design from specification to implementation. The lecture will introduce the theory of A/G Contracts and its latest development to support stochastic systems, optimization constraints, architectural specifications, etc. Then, it will provide an overview of the CHASE framework and it will show the application of the framework to the design and the analysis of different cyber physical systems.

Bio: Michele Lora is a Marie Skłodowska-Curie Fellow, holding a joint appointment at the University of Southern California and the University of Verona. Its fellowship aims at implementing the “Design automation for smart Factories” (DeFacto) project that will last until September 2023. The objective of the DeFacto project is to rethinking the design foundations of high-assurance intelligent manufacturing systems. He is also a co-founder of FACTORYAL, a start-up operating in the field of factory automation software.
He received the Ph.D. in Computer Science form the University of Verona in 2016. He also holds a M.Sc. degree in Computer Science and Engineering and a B.Sc. in Computer Science from the University of Verona. Between 2018 and 2020, he was a postdoctoral fellow at the ASSET Research Group of the Singapore University of Technology and Design (SUTD). During his Ph.D. he spent eight months in 2015 at the Donald O Pederson Center of the University of California, Berkeley; at Berkeley, he developed the first prototype of the CHASE framework. Michele is also a proud Erasmus alumnus: he spent one year in 2009 carrying on his research at the Embedded System Lab of the University of Linkoping in Sweden.

Alessandro Beghi - University of Padova, Italy

September 11 (13:30 – 15:00) – Nonlinear Model Predictive Control tools for real-time applications Control

Linear model predictive control (MPC) can be currently deployed in many application scenarios, due to the availability of very efficient algorithms for solving online quadratic programs. In contrast, nonlinear MPC (NMPC) requires the deployment of more elaborate algorithms, which require longer computation times than linear MPC. Nonetheless, computational speeds for NMPC comparable to those of MPC can be achieved, provided that the adequate algorithms are used. In this talk, we introduce the NMPC approach that is based on the real-time iteration (RTI) scheme, a technique that has been successfully tested and used in several applications, with computational burden that is sometimes comparable to that of MPC schemes. Some considerations regarding splitting of the algorithm cost in view of implementation on board of embedded devices will also be provided.

Bio: Alessandro Beghi received the Laurea degree cum laude in Electrical Engineering in 1989 and the Ph.D. degree in Control Systems Engineering in 1993, both from the University of Padova, Italy. In 1994 he joined the Department of Information Engineering, University of Padova, Italy, where he is currently a Full Professor of Control Systems Engineering and Chair of the Department Research Board. He held visiting positions at universities and international research centers both in Europe and in the USA. His research interests include modelling and control, filtering and identification, model reduction, fault detection and isolation, and their applications. He has worked on a wide range of control applications, from control of fusion devices, guidance algorithms for virtual vehicles, to control of HVAC&R systems, Adaptive Optics systems, and semiconductor manufacturing processes. He has been responsible of research projects funded by the European Union, the Italian Ministry for Instruction and Research, and the University of Padova. He has been responsible of research activities with national and international companies, among which, Electrolux, Emerson Network Power, Infineon, Aprilia Racing, Ducati Corse. He is co-inventor of 9 Patents on the use of advanced control techniques in different applications fields. He is a member of the Managing Board and scientific advisor of the Regional Industrial Cluster IMPROVENET “ICT for Manufacturing Processes Veneto Network”. He is the author of more than 200 publications in journals, books, and conference proceedings.

Marco Rocchetto – V-Research, Italy

September 11 (15:30 – 17:00) - Modeling Cyber-Physical System Cybersecurity: from Development Processes to Technical Architectures.

Cybersecurity in Cyber-Physical Systems (CPS) is of paramount importance. Cybersecurity attacks to CPS may impact safety-critical infrastructures to destabilize not just a business but national security. New EU regulations on OT technologies and then on CPS (such as the Machinery Regulation 2023/123) emphasize the impact that a lack of cybersecurity requirements may have on safety regulations. Most cybersecurity standards, such as the ISO 27001 and IEC 62443 (IACS), requires the design and enforcement of cybersecurity policies, procedures, and controls in the business processes, development processes, and within the technical architectures of CPS or OT technology produced or consumed by a company. To comply with cybersecurity standards and new EU regulations, companies are piling up documents over documents describing their security policies and processes, facing the impossible challenge to enforce (and verify) their documentation. The model-based approach presented in this talk shows that formal models, defining cybersecurity policies and procedures, are clearer, easier to maintain, and enabler for an automated model-based cybersecurity risk assessment (requested by most, if not all, cybersecurity standards). During the presentation, state-of-the-art languages and tools are discussed and applied to a reference CPS production process.

Bio: In 2009 he earned a M.S. in Computer Science at the University of Verona (Italy) and passed the State Qualifying Examination in Engineering at the University of Brescia (Italy). In 2014 he earned a PhD (Doctor Europeaus, visiting student at ETH Zurich) in Computer Science at the University of Verona (Italy). From 2010 to mid 2015 he held a research fellow position at the University of Verona (Italy) in the context of two EU-FP7 projects (AVANTSSAR and SpaCIoS). From 2015 to 2017 he held postdoctoral research fellow positions at the SUTD University (Singapore) and at the University of Luxembourg. In 2017 he joined, as a Senior Engineer, the Formal Methods group in the Research Center of the United Technologies Corp. In 2020 he co-founded V-Research, a private R&D center on cybersecurity.
Marco has several patent applications and publications in international scientific conferences and journals. He is reviewer and member of technical program committee of several international scientific workshops, conferences, and journals on cybersecurity. He worked as principal investigator and as main technical contributor in several public and private international research projects.

Davide Quaglia – University of Verona, Italy

September 12 (9:00, 10:30) - Network Specification and Design for Industrial CPS

The lecture consists of two parts. In the first part, I will present a formal approach to specify the communication requirements of a cyber-physical system so that the corresponding network infrastructure can be synthesized automatically. The methodology will be presented by using an example of industrial scenario. The second part will be devoted to describe the communication infrastructure of an Industry 4.0 shop floor and the safety mechanisms that it enables.

Bio: Davide Quaglia received his PhD in Computer Engineering from Politecnico di Torino (Italy) in 2003. Currently he is Associate Professor at the Computer Science Department of the University of Verona (Italy) where he currently teaches various courses on communication networks and network programming. He is author/co-author of about 70 papers and member of IEEE. He is member the technical program committee of ACM/IEEE DATE and Euromicro DSD. His current research interests include Networked Embedded Systems, Networked Control Systems, Cyber-Physical Systems and their applications to Internet of Things, Industry 4.0, smart cities and smart agriculture. He was also co-founder and collaborator of EDALab s.r.l., a spin-off company of the University of Verona.

Dong Seon Cheng – University of Verona, Italy

September 11 (11:00 – 12:30) – The Industrial Computer Engineering (ICE) Laboratory in action

The ICE Laboratory is a research facility meant to promote between the technological innovation of Industry 4.0 and the education and research centers located in the Verona area. The laboratory is equipped with a fully fledged production line actually capable of producing goods. This lecture will show, through a demonstration, the technologies implemented in the ICE laboratory in action. The demonstration will be accompanied by an in depth explanation about the integration of the different components in the laboratory, and it will show the reconfiguration abilities of the infrastructure discussing the implications on the scheduling of the production processes.

Bio: Cheng Dong Seon is a Research Associate at the University of Verona (Italy) from 2023. He acquired his Ph.D. in computer science (2008) with work in the field of computer vision and pattern recognition. Machine learning is his main interest, and he has published several conference and journal papers in the field. From 2012 to 2017, he was Assistant Professor at the Hankuk University of Foreign Studies (South Korea) teaching undergraduate and graduate courses in computer science. From 2019 to 2022 he has worked in the private sector for a company in the HVAC industry.

Frank Oppenheimer – OFFIS, Germany

Guest Lecture 1, September 13 (9:00 – 10:30) - With Digital Product Twin towards sustainable manufacturing

The lecture will discuss how digital twins can help to improve the efficiency of the resources used in manufacturing. After a brief motivation of the the importance of sustainability in manufacturing, we will take a closer look at Digital Product Twins (DPT). First, we will establish a common understanding of the widely used term Digital Twin and what makes Digital Product Twins special. Second, we will talk about the implementation of DPT - not only the technical perspective, but also the risks and challenges in its economic context. Finally, we will look at different application scenarios of DPT.

Bio: Since 2019, Frank Oppenheimer is the R&D Director in Manufacturing Division of OFFIS. His research focuses on Human-Machine Interaction, Sustainability in manufacturing, Industry 4.0 and distributed Cyber Physical Systems. Between 2008 and 2019, he was R&D Director in the Transportation Division of OFFIS where he was involved in multiple publicly funded projects. Between 2001 and 2008, he was group manager at OFFIS, leading the Hardware/Software Design Methodology Group, coordinating and managing several FP7 funded projects. Between 1998 and 2001 he was a researcher at the Carl Von Ossietzky Universitat, Oldenburg working at the DFG-funded project OOCOSIM.

Dr. Oppenheimer received his Ph.D. in Computer Science from the University of Oldenburg in 2005; his thesis focused on OOCOSIM: an object oriented co-design method for embedded HW/SW systems.

Michael Mendler – University of Bamberg

Guest Lecture 2, September 13. (14:00 – 15:30) - The Synchrony Hypothesis, Constructive Circuits and Timed Ternary Simulation

The synchronous model of programming (SP) emerged in the 1980ies. It has led to the development of well-known languages such as Statecharts, Esterel, Signal, Lustre, which make the programming of concurrent systems with deterministic and bounded reaction seem a routine exercise. The synchronous approach draws its success from the fact that it is founded on a simple and well-understood mathematical model of computation, the Mealy automaton. However, validity of this model is not for free. It depends on the Synchrony Hypothesis according to which a system is invariably faster than its environment. Yet, this raises a tangled compositionality problem. Since a node is in the environment of the every other node, it follows that each node must be faster than every other and hence faster than itself! At the technical level, the paradox of SP leads to cyclic boolean systems, which are non-monotonic and thus do not admit of a canonical least fixed-point semantics. Instead, many different compilation approaches have been proposed, making different assumptions about the implementation and stabilisation behaviour of the run-time architecture.
In this course, we discuss the logical foundations of the most prominent model of SP underlying Berry's Esterel, known as the "constructive semantics". This semantics is defined via ternary simulation, which is also a standard model for asynchronous circuits. We review the central result that constructive circuits are exactly those circuits for which signals settle to a unique value in bounded time, for any input, under a simple conservative delay model, called the up-bounded non-inertial (UN) delay. Hence, the UN-delay model constitutes an adequate electrical interpretation of ternary algebra. More specifically, these results provide a correctness and exactness result for the timing analysis of cyclic circuits such as the timed extension of Malik's or Brzozowski and Seger's pure ternary algorithm or the timed algorithm proposed by Riedel and Bruck, which originally were not formally linked with real-time execution models.
We contrast this with the traditional Muller theory for asynchronous circuits which uses the up-bounded inertial (UI) delay to justify ternary simulation. It can be shown that the match is not exact and that stabilization under the UI-delay model, in general, cannot be decided by ternary simulation. To explain these observations, we introduce Muller Logic, an axiomatic specification language for asynchronous circuits that mediates between the real-time behaviour and its abstract simulation in the discrete boolean domain. We conjecture that Muller Logic is sound and complete for the traditional "General Multiple Winner" semantics of asynchronous circuits under Muller's UI-delay model. Muller Logic is non-constructive, which is a result of the fact that it is expressive enough to specify memory and bounded non-determinism (arbitration). The restricted theory of constructive circuits corresponds to the UN-fragment of Muller logic, which is deterministic and cannot not express memory. Our logical characterisation easily explains why constructive circuits are delay-insensitive, i.e., invariant under arbitrary wire and gate delays.
Finally, we will suggest how full Muller Logic, and thus general UI-delay circuits, can be used to specify the semantics of sequentially-constructive Esterel. This language has recently been introduced to exploit the sequential nature of instruction set architectures, where Esterel’s constructive semantics targets concurrent hardware circuits.

Bio: Michael Mendler completed his PhD in the Laboratory for Foundations of Computer Science at Edinburgh University in 1993. He conducted postdoc research at Universities in Italy, Denmark and Germany and entered into academic teaching as Reader in Computer Science at Sheffield University, UK, in 1999. Since 2002 he is tenured professor and head of the Informatics Theory Group in the Faculty of Information Systems and Applied Computer Sciences at Bamberg University. Mendler's research interests are in the application of constructive logic, type theory and concurrency theory to programming language semantics and embedded systems. He has made internationally recognised contributions in the field of clocked process algebras for general concurrent systems and the causality and timing analysis of synchronous software and hardware, specifically developing compositional semantic methods addressing the causality problem arising from the Synchrony Hypothesis. His research was funded by the German Academic Research Council (DAAD), The British Council, British Engineering and Physical Sciences Research Council (EPSRC) and the German Research Foundation (DFG). The results have been published more than 90 (co-)authored peer-reviewed publications in book collections, international journals and conferences.

David Broman – KTH Royal Institute of Technology

Guest Lecture 3, September 14 (9:00 – 10:30) - Efficient Metaprogramming of Compilers for Domain-Specific Languages

Developing new compilers for programming and modeling languages can be a painstaking task, requiring both substantial engineering efforts and deep knowledge of compiler theory. Although domain-specific languages (DSLs) can make it easier for end-users to express their problems declaratively, the effort of engineering complete compilers can be a too large undertaking. An alternative is creating interpreters, which are simpler to develop but typically result in less efficient runtime environments. In this lecture, I will introduce the Miking framework that is designed to make it easy to develop efficient compilers for domain-specific languages. In particular, I will focus on three concepts: (i) statically resolvable ambiguity - a new way of writing parser, (ii) language fragment composition for quickly prototyping new semantics, and (iii) a new methodology for metaprogramming based on partial evaluation. The lecture will include both theory and practice, with many code examples.

Bio: David Broman is a Professor at the Department of Computer Science, KTH Royal Institute of Technology and an Associate Director Faculty for Digital Futures. He received his Ph.D. in Computer Science in 2010 from Linköping University, Sweden. Between 2012 and 2014, he was a visiting scholar at the University of California, Berkeley, where he also was employed as a part-time researcher until 2016. His research focuses on the intersection of (i) programming languages and compilers, (ii) real-time and cyber-physical systems, and (iii) probabilistic machine learning. David has received a Distinguished Artifact Award at ESOP (co-authored 2022), an outstanding paper award at RTAS (co-authored 2018), a best paper award in the journal Software & Systems Modeling (SoSyM award 2018), the award as teacher of the year, selected by the student union at KTH (2017), the best paper award at IoTDI (co-authored 2017), awarded the Swedish Foundation for Strategic Research's individual grant for future research leaders (2016), and the best paper presentation award at CSSE&T (2010). He has worked several years within the software industry, co-founded three companies, co-founded the EOOLT workshop series, and is a member of IFIP WG 2.4, Modelica Association, a senior member of IEEE, and a board member of Forskning och Framsteg.

Tutorials Speakers

Tutorials Speakers details.

Keynote Speakers

Keynote Speakers details.

Panel Speakers

Panel Speakers details.

FDL is in ,