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.
