“In the end, you are a mathematician, not a computer scientist” or “Have we not already discovered everything in computer science?”. Which theoretical computer scientist has not heard a similar sentence when trying to explain their research to a layperson? Promotion of theoretical computer science, and formal methods in particular, is mainly hindered by the high level of abstraction commonly used in the field, and probably furthermore complicated by a lack of education of the people thereupon. We present in this paper an educational experiment intended to explain the importance and aim of formal methods, along with the challenges they present. It uses LEGO R © robots as an anchor to the real world, introducing fun into the presentation. Primarily targeting high-school students, it forms a solid and adaptable basis to reach various audiences.

Pervasive computing systems can be modelled effectively as populations of interacting autonomous components. The key challenge to realizing such models is in getting separately-specified and -developed sub-systems to discover and interoperate with each other in an open and extensible way, supported by appropriate middleware services. In this paper, we argue that nature-inspired coordination models offer a promising way of addressing this challenge. We first frame the various dimensions along which nature-inspired coordination models can be defined, and survey the most relevant proposals in the area. We describe the nature-inspired coordination model developed within the SAPERE project as a synthesis of existing approaches, and show how it can effectively support the multifold requirements of modern and emerging pervasive services. We conclude by identifying what we think are the open research challenges in this area, and identify some research directions that we believe are promising.

The Computer After Me, pp. 159-172 (2014) No AccessChapter 11: The Social ComputerGiovanna Di Marzo Serugendo, Matteo Risoldi, and Mohammad SolemayniGiovanna Di Marzo SerugendoUniversity of Geneva, Switzerland, Matteo RisoldiUniversity of Luxembourg, Luxembourg, and Mohammad SolemayniImperial College London, UKhttps://doi.org/10.1142/9781783264186_0011Cited by:2 PreviousNext AboutSectionsPDF/EPUB ToolsAdd to favoritesDownload CitationsTrack CitationsRecommend to Library ShareShare onFacebookTwitterLinked InRedditEmail Abstract: The following sections are included: Introduction Problem and Research Questions State of the Art TSC Structure and Computational Awareness Methodology and Research Directions Case Study: Democracy Conclusions FiguresReferencesRelatedDetailsCited By 2Engineering Adaptivity, Universal Autonomous Systems Ethics and Compliance IssuesGiovanna Di Marzo Serugendo5 October 2016Advanced Manufacturing: An Industrial Application for Collective Adaptive SystemsDavid Sanderson, Nikolas Antzoulatos, Jack C. Chaplin, Didac Busquets and Jeremy Pitt et al.1 Sep 2015 The Computer After MeMetrics History PDF download

High-level Petri nets make models more concise and readable as compared to low-level Petri nets. However, usual verification techniques such as state space analysis remain an open challenge for both because of state space explosion. The contribution of this paper is to propose an approach for property based reduction of the state space of Algebraic Petri nets (a variant of high-level Petri nets). To achieve the objective, we propose a slicing algorithm for Algebraic Petri nets (APNSlicing). The proposed algorithm can alleviate state space even for certain strongly connected nets. By construction, it is guaranteed that the state space of sliced net is at most as big as the original net. We exemplify our technique through the running case study of car crash management system.

In Model-Driven Engineering, as in many engineering approaches, it is desireable to be able to assess the quality of a system or model as it evolves. A resilient engineering practice systematically assesses whether evolutions improve on the capabilities of a system. We argue that to achieve a systematic resilient model-driven engineering practice, resilience concepts should be first-class citizens in models. This article discusses how DREF, a formal framework defining resilience concepts, can be integrated with other modeling languages in order to pursue a resilient development process.

The dynamics of pervasive ecosystems are typically highly unpredictable, and therefore self-organising approaches are often exploited to make their applications resilient to changes and failures. The SAPERE approach we illustrate in this paper aims at addressing this issue by taking inspiration from natural ecosystems, which are regulated by a limited set of "laws" evolving the population of individuals in a self-organising way. Analogously, in our approach, a set of so-called eco-laws coordinate the individuals of the pervasive computing system (humans, devices, signals), in a way that is shown to be expressive enough to model and implement interesting real-life scenarios. We exemplify the proposed framework discussing a crowd evacuation application, tuning and validating it by simulation.

Here we present the overall objectives and approach of the SAPERE (“Self-aware Pervasive Service Ecosystems”) project, focussed on the development of a highly-innovative nature-inspired framework, suited for the decentralized deployment, execution, and management, of self-aware and adaptive pervasive services in future network scenarios.

Although model checking is heavily used in the hardware domain, it did not take off in software engineering yet. One of the possible reasons is that software models are very complex. They integrate many dimensions such as data types and concurrency, leading to the infamous state space explosion problem. This article introduces the Algebraic Petri Nets Analyzer (AlPiNA), a symbolic model checker for High-level Petri nets. It is comprised of two independent modules: a GUI plug-in for Eclipse and an underlying model checking engine. AlPiNA is a step towards performing efficient and user-friendly model checking of large software systems. This is achieved by separating the model and its properties from the optimisation artifacts. This article describes the features that AlPiNA provides to the user for designing models and verifying properties. It also presents the techniques and artifacts used for tuning verification performance, along with some theoretical background.

The behaviour of self-* systems is complex to model from an algorithmic point of view.Designing and specifying self-* systems implies a great amount of work that can be sensibly reduced if models can be reused and composed in a modular way.This article discusses a chemicallyinspired architecture and formalisms that facilitate the creation of modular, reusable models based on behavioural patterns inspired by behaviours found in nature.The architecture is based on chemical-like laws ruling the evolution of the system.We show the reuse of general behavioural patterns using three concrete examples of self-* systems from different domains.

Here we present the overall objectives and approach of the SAPERE (Self-aware Pervasive Service Ecosystems) project, focussed on the development of a highly-innovative nature-inspired framework, suited for the decentralized deployment, execution, and management, of self-aware and adaptive pervasive services in future network scenarios. © Selection and peer-review under responsibility of FET11 conference organizers and published by Elsevier B.V. 1. Motivations Pervasive computing technologies promise to notably change the future ICT landscape, letting us envision the emergence of an integrated and very dense socio-technical infrastructure for the provisioning of innovative general- purpose digital services. The infrastructure will be used to ubiquitously access services for better interacting with the surrounding physical world and with the social activities occurring in it. It is also expected that users will be able to deploy customized services, making the overall infrastructure as open as the Web currently is. To support the vision, a great deal of research activity in pervasive computing and service systems has been devoted to solve problems such as: increasing dependability; supporting self-* features; enforcing context-awareness and adaptability; tolerating evolution over time and eventually ensuring that service frameworks can be highly-adaptive and very long-lasting (1). Unfortunately, most of the solutions so far are proposed in terms of add-ons to be integrated in existing frameworks. The result is often an increased complexity of current frameworks and the emergence of contrasting trade-off between different solutions. In our opinion, there is need for tackling the problem at the foundation, answering the following ambitious question: is it possible to conceive a radically new way of modeling integrated pervasive services and their execution environments, such that the apparently diverse issues of context-awareness, dependability, openness, flexible and robust evolution, can all be uniformly addressed once and for all?

AlPiNA is a symbolic model checker for High Level Petri nets. It is comprised of two independent modules: a GUI plugin for Eclipse and an underlying model checking engine. AlPiNA’s objective is to perform efficient and user-friendly, easy to use model checking of large software systems. This is achieved by separating the model and its properties from the model checking-related concerns: the users can describe and perform checks on a high-level model without having to master low-level techniques. This article describes the features that AlPiNA provides to the user for specifying models and properties to validate, followed by the techniques that it implements for tuning validation performance.

AlPiNA is a graphical editor and model checker for a class of high-level Petri nets called Algebraic Petri Nets. Its main purpose is to perform reachability checks on complex models. It performs symbolic model checking based on ΣDD, an efficient evolution in the Decision Diagrams field, using novel techniques such as algebraic clustering and algebraic unfolding. AlPiNA offers a user-friendly interface, and is easily extensible.

Benchmarking is a fundamental activity to rigorously quantify the im- provements of a new approach or tool with respect to the state of the art. Gen- erally, it consists in comparing results of a given technique with more or less similar approaches. In the Petri nets community, the comparison is often centered on model checking and/or state space calculation performance. However, there is sometimes little justification for the choice of the techniques to compare to. Also, benchmarks often lack context information, such as the exact model used, or how to reproduce the results. This makes it di cult to draw conclusions from the comparisons. We conducted a survey among the Petri nets community in which we gathered in- formation about the used formalisms and techniques. This revealed an unanimous interest for a common repository of benchmarks. The survey shows that existing e orts in this direction su er from limitations that prevent their e ectiveness. In this article we report the results of the survey and we outline perspectives for improving Petri nets benchmark repositories.

Decision Diagrams (DDs) are a well populated family of data structures, used for ecient representation and manipulation of huge data sets. Typically a given application requires choosing one particular category of DDs, like Binary Decision Diagrams (BDDs) or Data Decision Diagrams (DDDs), and sticking with it. Each category provides a language to specify its operations. For instance, the operation language of BDDs provides if-then-else, apply, etc. We focus on two main kinds of operation languages: BDD-like and DDD- like. They overlap: some operations can be expressed in both kinds of languages, while others are only available in one kind. We propose in this article a critical comparison of BDD-like and DDD- like languages. From the identified problems, we also propose a unified language for DD operations. It covers both BDD-like and DDD-like lan- guages, and even some operations that cannot be expressed in either.

Designing a DSML implies binding the syntactical concepts of the problem domain with the semantics of a solution domain. Previous work presented a formal framework for language composition where language syntactical patterns (expressed by metamodels) along with their semantics (expressed by transformation models) are combined as small reusable building blocks in a constructive manner, in order to achieve the desired expressiveness for DSMLs. This article refines the framework, as well as showing its application through a case study led in collaboration with CERN (European Organization for Nuclear Research).

The software development process of user interfaces for complex control system can constantly change in requirements. In those systems changes are costly (time consuming) and error prone, since we must guarantee that the resulting system implementation will still be robust and reliable. A way to tackle this problem is to bring a software model based approach for specification and providing at the same time rapid prototyping capabilities (to speed up design) and Simulation/Verification capabilities (to assure quality). We propose a full model-based methodology to guide designers through specification changes.

The BATIC3S project (Building Adaptive Three-dimensional Interfaces for Controlling Complex Control Systems) proposes a methodology to prototype adaptive graphical user interfaces (GUI) for control systems. We present a domain specific language for the control systems domain, including useful and understandable abstractions for domain experts. This is coupled with a methodology for validation, verification and automatic GUI prototype generation. The methodology is centered on metamodel-based techniques and model transformations, and its foundations rely on formal models. Our approach is based on the assumption that a GUI can be induced from the characteristics of the system to control.