nach oben

2020 | Buch

Kapitel lesen Erstes Kapitel lesen

Software Engineering and Formal Methods

SEFM 2019 Collocated Workshops: CoSim-CPS, ASYDE, CIFMA, and FOCLASA, Oslo, Norway, September 16–20, 2019, Revised Selected Papers

herausgegeben von: Dr. Javier Camara, Martin Steffen

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

The volume LNCS 12226 constitutes the revised selected papers from the four workshops collocated with the 17th International Conference on Software Engineering and Formal Methods, SEFM 2019.

The 13 full papers presented together with 7 short papers in this volume were carefully reviewed and selected from a total of 45 submissions. They stem from the following workshops:

CoSim-CPS 2019 – 3rd International Workshop on Formal Co-Simulation of Cyber-Physical Systems; ASYDE 2019 -- 1st International Workshop on Cognition: Interdisciplinary Foundations, Models and Applications; and FOCLASA 2019 -- 17th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems.

Inhaltsverzeichnis

Frontmatter

CoSim-CPS 2019

Frontmatter

Co-simulation and Verification of a Non-linear Control System for Cogging Torque Reduction in Brushless Motors

Abstract

This work aims at demonstrating the benefits of integrating co-simulation and formal verification in the standard design flow of a brushless power drive system for precision robotic applications. A sufficient condition on controller gain for system stability is derived from the system’s mathematical model, including a control algorithm for the reduction of cogging torque. Then, using co-simulation and design space exploration, fine tuning of the controller gain parameters has been executed, exploiting the results from the formal verification.

Cinzia Bernardeschi, Pierpaolo Dini, Andrea Domenici, Sergio Saponara

Challenges for Integrating Humans into Vehicular Cyber-Physical Systems

Abstract

Advances in Vehicular Cyber-Physical Systems (VCPS) are the primary enablers of the shift from no automation to fully autonomous vehicles (AVs). One of the impacts of this shift is to develop safe AVs in which most or all of the functions of the human driver are replaced with an intelligent system. However, while some progress has been made in equipping AVs with advanced AI capabilities, VCPS designers are still faced with the challenge of designing trustworthy AVs that are in sync with the unpredictable behaviours of humans. In order to address this challenge, we present a model that describes how a Human Ambassador component can be integrated into the overall design of a new generation of VCPS. A scenario is presented to demonstrate how the model can work in practice. Formalisation and co-simulation challenges associated with integrating the Human Ambassador component and future work we are undertaking are also discussed.

Sulayman K. Sowe, Martin Fränzle, Jan-Patrick Osterloh, Alexander Trende, Lars Weber, Andreas Lüdtke

Automatic Generation of Functional Mock-Up Units from Formal Specifications

Abstract

This paper reports on the approach used to augment a transition system tool with automatic Functional Mock-up Units (FMU) generation. To verify the FMU properties, the same transition system can be translated into a formal language. Among intrinsic system properties, transition systems are associated with the following two: the disjointedness and the coverage, which assert that the controller is deterministic and defined for every possible input. This paper shows how both properties are enforced when proving the type checking conditions derived by the PVS theorem prover.

Maurizio Palmieri, Hugo Daniel Macedo

Generation of Co-simulation Algorithms Subject to Simulator Contracts

Abstract

Correct co-simulation results require a careful consideration of how the interacting simulators are implemented. In version 2.0 of the FMI Standard, input handling implementation is left implicit, which leads to the situation where a simulator can be interacted with in a manner that its implementation does not expect, yielding incorrect results.

In this paper, we build on prior work to make information about each simulator implementation explicit, in order to derive correct interactions with it. The formalization we use is specific to two kinds of contracts, but could serve as a basis to a general approach to black box co-simulation. The algorithm we propose generates a co-simulation execution plan in linear time. It has been successfully applied to an industrial case study, and the results are available online.

Cláudio Gomes, Casper Thule, Levi Lúcio, Hans Vangheluwe, Peter Gorm Larsen

Towards Reuse of Synchronization Algorithms in Co-simulation Frameworks

Abstract

An immediate industry challenge is to fashion a co-simulation that replicates real-systems behaviour with high fidelity. To achieve this goal, developers rely on frameworks to enhance the creation and analysis of the co-simulation. One major problem is that new co-simulation frameworks require extensive development, most of which resides in non-essential functionalities, before they can be used in practice. Additionally, existing co-simulations demand a thorough understanding before they can be extended.

Our vision is a modular co-simulation framework architecture, that is easily extensible by researchers, and can integrate existing and legacy co-simulation approaches. The architecture we propose permits extension at three levels, each providing different degrees of flexibility. The most flexible integration level involves the specification of a Domain Specific Language (DSL) for Master Algorithms (MAs), and this paper sketc.hes such a DSL, and illustrates how it is expressive enough to describe well-known MAs.

Casper Thule, Maurizio Palmieri, Cláudio Gomes, Kenneth Lausdahl, Hugo Daniel Macedo, Nick Battle, Peter Gorm Larsen

ASYDE 2019

Frontmatter

Towards a Continuous Model-Based Engineering Process for QoS-Aware Self-adaptive Systems

Abstract

Modern information systems connecting software, physical systems, and people, are usually characterized by high dynamism. These dynamics introduce uncertainties, which in turn may harm the quality of service and lead to incomplete, inaccurate, and unreliable results. In this context, self-adaptation is considered as an effective approach for managing run-time uncertainty. However, classical approaches for quality engineering are not suitable to deal with run-time adaptation, as they are mainly used to derive the steady-state solutions of a system at design-time. In this paper, we envision a Continuous Model-based Engineering Process that makes use of architectural analysis in conjunction with experimentation to have a wider understanding of the system under development. These two activities are performed incrementally, and jointly used in a feedback loop to provide insights about the quality of the system-to-be.

Mirko D’Angelo, Lorenzo Pagliari, Mauro Caporuscio, Raffaela Mirandola, Catia Trubiani

Automated Feature Identification for Android Apps

Abstract

Mobile apps are becoming increasingly complex, as nowadays a growing amount of apps no longer focuses on being a “specialized utility” but acts as an “all-around” app that offers assorted features (e.g., news feed, messaging, weather, map, and navigation, etc.). In this paper, we argue that being able to automatically and precisely identify the features offered by an app would allow researchers to investigate new technical solutions, that in turn would benefit both end-users, developers and, researchers. As a stepping stone in this direction, we describe an automated technique to identify features within Android apps. Our approach performs the identification of the features by extracting information from the app user interface and grouping together semantically similar concepts thanks to knowledge-base aided natural text processing and machine learning.

Gian Luca Scoccia

Mapping BPMN2 Service Choreographies to Colored Petri Nets

Abstract

Nowadays, software systems are often built by reusing and integrating existing services distributed over the Internet. Service choreography is a service engineering approach to compose together and coordinate services by specifying their external interactions in terms of flows of peer-to-peer message exchanges, given from a global perspective. BPMN2 offers a dedicated notation, called Choreography Diagrams, to specify service choreographies. However, BPMN2 specifications lack formal semantics causing some misinterpretations by practitioners and researchers. Colored Petri Net (CPN) is a formally proved notation with mathematical semantics and tool support for different analysis techniques. In this paper, we present a mapping to transform BPMN2 Choreography Diagrams into Colored Choreography Nets (CCNs). The latter is a CPN for enabling simulation and analysis of servicechoreographies.

Tala Najem, Alexander Perucci

CIFMA 2019

Frontmatter

Interdisciplinary Aspects of Cognition

Abstract

This position paper analyses the multidisciplinarity of cognitive research and its challenges from three perspective: the foundations of cognitive science, which draw from logic and neuroscience and their interconnections in studying human logic; computation as a means to identify mathematical patterns in human cognition, represent them symbolically and use such representations in computer emulations of human cognitive activities and possibly verify properties of such activities; education, devising and implementing learning models that exploit as well as address human cognition.

Antonio Cerone, Siamac Fazli, Kathy L. Malone, Ahti-Veikko Pietarinen

A Trust Logic for the Varieties of Trust

Abstract

In his paper Varieties of Trust, Eric Uslaner presents a conceptual analysis of trust with the aim of capturing the multiple dimensions that can characterize various notions of trust. While Uslaner’s analysis is theoretically very useful to better understand the phenomenon of trust, his account is rarely considered when formal conceptions of trust are built. This is often due to the fact that formal frameworks concentrate on specific aspects of phenomena rather than general features and, thus, there is little space for omni-comprehensive considerations about concepts. However, building formal languages that can describe trust generally are extremely important, since they can provide basic accounts employable as starting points for further investigations on trust. This paper addresses exactly this issue by providing a logical language expressive enough to describe all the varieties of trust derivable from Uslaner’s conceptual analysis. Specifically, Uslaner’s analysis is transformed into a conceptual map of trust, by strengthening his analysis with further reflections on the nature of trust. Then, a logical language for trust is introduced and it is shown how the validity classes of such language can characterize all the varieties of trust derivable from the conceptual map previously built.

Mirko Tagliaferri, Alessandro Aldini

Open Access

Behaviour and Reasoning Description Language (BRDL)

Abstract

In this paper we present a basic language for describing human behaviour and reasoning and present the cognitive architecture underlying the semantics of the language. The language is illustrated through a number of examples showing its ability to model human reasoning, problem solving, deliberate behaviour and automatic behaviour. We expect that the simple notation and its intuitive semantics may address the needs of practitioners from non matematical backgrounds, in particular psychologists, linguists and other social scientists. The language usage is twofold, aiming at the formal modelling and analysis of interactive systems and the comparison and validation of alternative models of memory and cognition.

Antonio Cerone

PDF Zum Volltext

Cognitive Learning with a Robot: The Case of Script Acquisition

Abstract

This research is situated in a specialized context offering a rarely occurring opportunity for research questions and technical objectives about language acquisition. The Kazakh language transition from Cyrillic to Latin alphabet in Kazakhstan raises challenges to teach the whole population to write and read in the new script. We propose an unique interdisciplinary approach by integrating innovative solutions from robotics, computer vision fields and pedagogical strategies from education, linguistics and cognitive sciences that will assist various demographic groups in this challenging endeavor. This paper presents the proposed system—a human-robot interaction application designed to assist primary school children in learning a new script and its associated handwriting. The system was deployed in a series of experiments where children increase their knowledge of the new script when practicing handwriting with a robot.

Anara Sandygulova, Anna CohenMiller, Nurziya Oralbayeva, Wafa Johal, Thibault Asselborn, Pierre Dillenbourg

Measuring the Intelligence of an Idealized Mechanical Knowing Agent

Abstract

We define a notion of the intelligence level of an idealized mechanical knowing agent. This is motivated by efforts within artificial intelligence research to define real-number intelligence levels of complicated intelligent systems. Our agents are more idealized, which allows us to define a much simpler measure of intelligence level for them. In short, we define the intelligence level of a mechanical knowing agent to be the supremum of the computable ordinals that have codes the agent knows to be codes of computable ordinals. We prove that if one agent knows certain things about another agent, then the former necessarily has a higher intelligence level than the latter. This allows our intelligence notion to serve as a stepping stone to obtain results which, by themselves, are not stated in terms of our intelligence notion (results of potential interest even to readers totally skeptical that our notion correctly captures intelligence). As an application, we argue that these results comprise evidence against the possibility of intelligence explosion (that is, the notion that sufficiently intelligent machines will eventually be capable of designing even more intelligent machines, which can then design even more intelligent machines, and so on).

Samuel Allen Alexander

Type Theory and Universal Grammar

Abstract

The idea of Universal Grammar (UG) as the hypothetical linguistic structure shared by all human languages harkens back at least to the 13th century. The best known modern elaborations of the idea are due to Chomsky. Following a devastating critique from theoretical, typological and field linguistics, these elaborations, the idea of UG itself and the more general idea of language universals stand untenable and are largely abandoned. The proposal tackles the hypothetical contents of UG using dependent and polymorphic type theory in a framework very different from the Chomskyan one(s). Linguistic-typologically, the key novelty is introducing universal supercategories (categories of categories) for natural language modeling. Type-theoretically, we introduce a typed logic for a precise, universal and parsimonious representation of natural language morphosyntax and compositional semantics. The implementation of the logic in the Coq proof assistant handles grammatical ambiguity (with polymorphic types), selectional restrictions, quantifiers, adjectives and many other categories with a partly universal set of types.

Erkki Luuk

Two Cognitive Systems, Two Implications, and Selection Tasks

Abstract

Dual-process theories of reasoning take for granted the fundamental difference between the two cognitive systems, Systems 1 and 2. This paper, in contrast, argues that System 1, which is responsible for fast, intuitive, associative, and effortless reasoning, can be explained to be just as logical as System 2, which is said to draw consequences in rule-based, rational and criticised fashions. The only difference between the two systems is argued to be that the former draws conclusions in a logic which is diagrammatic, and moreover a positive and implicational fragment of ordinary, classical logic. Such a fundamental connection between the two systems is then applied to explain away cognitive biases in the Wason card selection task. The selection task thus ceases to represent a paradigm case of confirmation bias, because both systems of reasoning exhibit important processes of logical inferences.

Angelina Bobrova, Ahti-Veikko Pietarinen

FOCLASA 2019

Frontmatter

Quantifying the Similarity of Non-bisimilar Labelled Transition Systems

Abstract

Equivalence checking is an established technique for automatically verifying that two behavioural models (Labelled Transition Systems, LTSs) are equivalent from the point of view of an external observer. When these models are not equivalent, the checker returns a Boolean result with a counterexample, which is a sequence of actions leading to a state where the equivalence relation is not satisfied. However, this counterexample does not give any indication of how far the two LTSs are one from another. One can wonder whether they are almost identical or totally different, which is quite different from a design or debugging point of view. In this paper, we present an approach for measuring the similarity between two LTS models. The set of metrics is computed automatically using a tool we implemented. Beyond presenting the foundations of the proposed solution, we will show how it can be applied to a concrete application domain for supporting the construction of IoT applications by composition of existing devices.

Gwen Salaün

Identifying Failure Causalities in Multi-component Applications

Abstract

Understanding and resolving failure causalities in modern enterprise applications is one of the main challenges daily faced by application administrators. Such applications indeed integrate multiple heterogeneous components, and identifying which components are causing the failure of which other components requires to delve through distributed application logs. In this work-in-progress paper, we present our idea of devising an analysis approach based on management protocols, a fault-aware compositional modelling for the management of multi-component applications. We discuss how they can be used to identify causalities of failures in multi-component applications, and to design countermeasures to avoid (or, at least, limit) failure propagation.

Antonio Brogi, Jacopo Soldani

A Formal Programming Framework for Digital Avatars

Abstract

In the current IoT era, the number of smart things to interact with is raising everyday. However, each one of them precises a manual and specific configuration. In a more people-friendly scenario, smart things should adapt automatically to the preferences of their users. In this field, we have participated in the design of People as a Service, a mobile computing reference architecture which endows the smartphone with the capability of inferring and sharing a virtual profile of its owner. Currently, we are developing Digital Avatars, a framework for programming interactions between smartphones and other devices. This way, the smartphone becomes a personalized and seamless interface between people and their IoT environment, configuring the smart things with information from the virtual profile. In this work, we present a formalization of Digital Avatars by means of a Linda-based system with multiple shared tuple spaces.

Alejandro Pérez-Vereda, Carlos Canal, Ernesto Pimentel

Modeling Self-adaptive Fog Systems Using Bigraphs

Abstract

Fog systems are a recent trend of distributed computing having vastly ubiquitous architectures and distinct requirements making their design difficult and complex. Fog computing is based on an idea that consists of leveraging both resource-scarce computing nodes around the Edge to perform latency and delay sensitive tasks and Cloud servers for the more intensive computation. A convenient way to address the challenge of designing Fog systems is through the use of formal methods, which provide the needed precision and high-level assurance for their specification through formal verification. In this paper, we present a novel formal model defining spatial and structural aspects of Fog-based systems using Bigraphical Reactive Systems, a fully graphical process algebraic formalism. The model is extended with reaction rules to represent the dynamic behavior of Fog systems in terms of self-adaptation. The notion of bigraph patterns is used in conjunction with boolean and temporal operators to encode spatio-temporal properties inherent to Fog systems and applications. The feasibility of the modelling approach is demonstrated via a motivating case study and various self-adaptation scenarios.

Hamza Sahli, Thomas Ledoux, Éric Rutten

From SOS to Asynchronously Communicating Actors

Abstract

Structural Operational Semantics (SOS) provides a general format to describe a model as a transition system with very powerful synchronization mechanisms. Actor systems are distributed, asynchronously communicating units of computation with encapsulated state, with much weaker means of synchronizing between actors. In this paper, we discuss an implementation of a SOS model using actors in the object-oriented actor language ABS and how to argue that global properties about the model are inherited from the SOS level to the actor implementation. The work stems from a case study modelling the memory system of a cache-coherent multicore architecture.

Frank de Boer, Einar Broch Johnsen, Ka I Pun, Silvia Lizeth Tapia Tarifa

Backmatter

Titel: Software Engineering and Formal Methods
herausgegeben von: Dr. Javier Camara
Martin Steffen
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-57506-9
Print ISBN: 978-3-030-57505-2
DOI: https://doi.org/10.1007/978-3-030-57506-9