FAACS @ ECSA 2019

• 08:15 - 09:15: Registration
• 09:15 - 9:30: Opening (session chair: Matteo Camilli)
• 09:30 - 10:30: Keynote speech (session chair: Matteo Camilli)
• Javier Camara: Model Integration and Decision-Making for Self-Adaptation in Mobile Robotics
• 10:30 - 11:00: Coffee Break
• 11:00 - 12:30: Paper session 1: Stochastic approaches for Cyber Physical Systems (session chair: Javier Camara)
• Jacques Malenfant: Stochastic Hybrid Systems Meet Software Components for Well-Founded Cyber-Physical Systems Software Architectures
• Lorenzo Pagliari, Mirko D'Angelo, Mauro Caporuscio, Raffaela Mirandola and Catia Trubiani: To What Extent Formal Methods are Applicable for Performance Analysis of Smart Cyber-Physical Systems?
• 12:30 - 14:00: Lunch
• 14:00 - 15:30: Paper session 2: Formal methods to design Distributed Systems (session chair: Patrizia Scandurra)
• Paolo Gaspari, Elvinia Riccobene and Angelo Gargantini: A formal design of the Hybrid European Rail Traffic Management System
• Nuno Santos, Carlos E. Salgado, Helena Rodrigues, Francisco Morais, Mónica Melo, Sara Silva, Raquel Martins, Marco Pereira, Nuno Ferreira, Manuel Pereira and Ricardo J. Machado: A logical architecture design method for microservices architectures
• 15:30 - 16:00: Coffee Break
• 16:00 - 16:45: Paper session 3: Smart solutions to design IoT Systems (session chair: Elvinia Riccobene)
• Mohammad Sharaf, Mai Abusair, Rami Ilawi, Yara Shana'A, Ithar Saleh and Henry Muccini: Architecture Description Language for Climate Smart Agriculture Systems
• 16:45 - 17:00: Discussion and wrap up session (session chair: Matteo Camilli)

Javier Cámara is a Lecturer in the Department of Computer Science at the University of York (UK). Prior to being a Lecturer in York, he has been a Senior Research Scientist at Carnegie Mellon University (USA), where he held technical leadership responsibilities in projects that explored the construction and formal analysis of self-managing systems by combining quantitative verification, game-theoretical models, and formal descriptions of software architectures. He has applied these techniques in projects that span the mobile robotics, Cyber Security, and Systems-of-Systems domains. He graduated from the University of Granada (Spain) and worked for two years as a software engineer before starting graduate school. After receiving his Ph.D. in Computer Science from the University of Málaga (Spain), he worked as a postdoctoral researcher at INRIA Rhône-Alpes (France), and the University of Coimbra (Portugal).

Title: Model Integration and Decision-Making for Self-Adaptation in Mobile Robotics

Abstract: Software Engineering today is increasingly faced with the challenge of creating systems that involve both software and physical systems -- or CPS -- from robotic systems, to autonomous vehicles, to increasingly sophisticated medical devices. In such systems, physical and software components are deeply intertwined, each operating on different spatial and temporal scales, exhibiting multiple and distinct behavioral modalities, and interacting with each other in a myriad of ways that change with context. CPS often need to self-adapt their structure and behavior at run time to respond to changes in their operating environment. Existing approaches to engineering self-adaptation have at their core a set of models used to support reasoning about when and how to best adapt the system at run time. Combining information from such models to feed run-time analysis and planning processes for self-adaptation in pure software systems is relatively straightforward because all the models describe software. However, models in a CPS are much more heterogeneous in terms of representation, semantics, and facet of the domain that they capture (e.g., energy consumption, software architecture, physical space, safety). This heterogeneity poses a fundamental challenge in bringing together the information represented in these models to support self-adaptation in CPS. This challenge is complicated by the inherent uncertainty that arises both from the imprecision of the models, as well as the variability and lack of predictability of the environment. This talk provides an overview of a model-based synthesis and quantitative verification approach to decision-making for self-adaptation that has been applied to the domain of mobile service robots. The approach: (a) abstracts relevant information into views from heterogeneous models, and integrates them into high-level probabilistic models; and (b) incorporates planning that has at its core a probabilistic model checker (PRISM) that is used to reason quantitatively about the outcome of adaptation decisions in a rich trade-off space. The key benefits of this approach are extensibility (new types of models can be added), generality (the planning mechanism allows an arbitrary number of quantifiable quality dimensions), assurance (the probabilistic planner provides quantitative guarantees about behavior), and automation (system reconfiguration actions and task planning can be directly synthesized from models).