(click on the talk title to see the abstract and the presenter’s bio)
Tiziana Margaria (University of Limerick, Confirm and Lero, Ireland)
“The Role of Models as Digital Twins of Smart Processes, Machines and Parts in Industry 4.0”
Abstract: In the Confirm research centre on Smart Manufacturing as well as in Industry 4.0 in general, a Digital Thread connects the data and processes for smarter products, smarter production, and smarter integrated ecosystems. While the tangible goods (products and production lines) are understood as needing a Digital Twin as an executable model, i.e. an in-silico entity on which to virtually explore design, production, quality, and lifetime maintenance, the immaterial goods like software are not yet treated on par.
We argue that the increasingly ambitious needs of the people, the economic sectors, and the large-scale trends can only be met if the IT professions embrace and adopt a new way of producing and consuming IT. The new way to deal with software will be more mature in the sense of automation of production and management, based on more formal descriptions, more models, more reasoning and analysis before expensive implementations are incurred. Behavioural models are accordingly the natural Digital Twins of the software.
For this new paradigm to enter mainstream, models need to be coupled with automatic transformations, generations, and analyses that take advantage of the formalized knowledge about the immaterial and material entities. This formalized knowledge includes a variety of models together wit Domain Specific Languages that use semantic types at their core.
We provide a few examples of how the new thinking can disrupt the status quo but empower a better understanding, a more efficient organization, and a more automatic management of the many cross-dimensional issues that future connected software and systems will depend upon.
Bio: Professor Tiziana Margaria is Chair of Software Engineering and Head of Department at the Dept. of Computer Science and Information Systems at the University of Limerick. She also heads the Lero Committee on International Relations Development.
She has broad experience in the use of formal methods for high assurance systems, in particular concerning functional verification, reliability, and compliance of complex heterogeneous systems.
She is currently Vice President of the European Association of Software Science and Technology (EASST); President of FMICS (the ERCIM Working Group on Formal Methods for Industrial Critical Systems); steering committee member of ETAPS, the European joint Conferences on Theory and Practice of Software; managing editor of STTT, the Springer Journal on Software Tools for Technology Transfer; and co-founder of the TACAS and ISoLA series of conferences. Tiziana is a Fellow of the Irish Computer Society and of SDPS, the Society for Design and Process Science.
In EuSEM (European Society for Emergency Medicine), she co-chairs the Special Interest Group on Technology and Processes of Care in the Emergency Care (SIG-TPCEC).
In Lero, she heads research projects on Scientific Workflows, in particular for data analytics, on model-driven service-oriented Software design for evolving systems, and on holistic HW/SW Cybersecurity. Current application domains are to embedded systems, healthcare, and smart advanced manufacturing. The aforementioned are Tiziana’s research topics and application domains most relevant to ALECS.
Presentation slides: 
Valeriy Vyatkin (Aalto University, Finland and Luleå University of Technology, Sweden)
“Cyber-Physical Components as building blocks of more dependable industrial CPS”
Abstract: This talk reflects upon 20 years long efforts of the speaker to apply model-checking based formal verification to the practice of industrial automation. These efforts were mainly happening in the academia with sporadic attempts to interact with industry.
From the very beginning the closed-loop view on the systems under verification was taken.
Early works on the application of model-checking to verification of programs date back to early 90s, and the first works on closed-loop verification appeared a few years after, in the end of 90s.
The reason behind the closed-loop approach is two-fold. First and foremost, explicit modelling of the plant enables formulation of requirements in terms of the plant’s processes which makes more sense for the automation system owner.
Another reason is that the closed-loop pattern promises lower complexity of model-checking than that of open-loop systems.
Another feature of the modern automation systems is modularity, and this feature is becoming increasingly more obvious. This requires modularization and “aspectisation” of the formal models as well, leading to the concept of cyber-physical component as an artefact used in both engineering and verification. To increase industrial applicability of this concept, we tried to rely on industrial standards for defining the input to our verification tools.
The fundamental question in the closed-loop approach is how to develop models of the plant systematically and with less effort. In recent works we explored ideas of using simulation models as a source for generating automatically discrete state models using evolutionary algorithms or other heuristics. We also tried to limit evolutions of the plant to those which the controller under verification could bring the plant to, trying to “infuse” non-determinism on a limited scale.
The talk will touch upon several techniques aiming at practical applicability of model-checking and its use by the practicing control engineers.
Bio: (IEEE M’03–SM’04) is on joint appointment as Chaired Professor (Ämnesföreträdare) of Dependable Computation and Communication Systems at Luleå University of Technology, Sweden, and Professor of Information and Computer Engineering in Automation, Aalto University, Finland. He is also co-director of the international laboratory of Computer Technologies at ITMO University, Saint-Petersburg, Russia.
Previously he has been with Cambridge University, U.K., as a visiting scholar, and on permanent academic appointments with The University of Auckland, New Zealand, Martin Luther University of Halle-Wittenberg, Germany, and with Taganrog State University of Radio Engineering, and postdoc at Nagoya Institute of Technology, Japan.
Valeriy graduated in applied computer science and obtained Ph.D. from Taganrog State Radio Engineering University in Russia.
Current research interests of Dr. Vyatkin include dependable distributed automation and industrial informatics, software engineering for industrial automation systems, distributed architectures, applied in various industry sectors, including Smart Grid, material handling, building management systems, and reconfigurable manufacturing. He is also active in research on dependability provisions for industrial automation systems, such as methods of formal verification and validation, and theoretical algorithms for improving their performance.
Dr. Vyatkin was awarded the Andrew P. Sage Award for the best IEEE Transactions paper in 2012.
Presentation slides:
