Application development for the modern web involves sophisticated engineering workflows—including user interface (UI) aspects. Such user interfaces comprise web elements that are typically created with HTML/CSS markup and JavaScript-like languages, yielding web documents. Their testing entails performing checks to examine visual and structural parts of the resulting UI software against requirements such as usability, accessibility, performance, or, increasingly, compliance with standards. However, current techniques are largely ad hoc and tailor-made to specific classes of requirements or web technologies and extensively require human-in-the-loop qualitative evaluations. Web UI evaluation so far has lacked formal foundations, which would provide assurances of compliance with requirements in an automatic manner. To this end, we devise a methodology and accompanying technical framework for web UIs. In our approach, requirements are formally specified in a spatio-temporal logic able to capture both the layout of visual components as well as how they change over time, as a user interacts with them. The technique we advocate is independent of the underlying technologies a web application may be developed with, as well as the browser and operating system used. To concretely support the specification and evaluation of UI requirements, our framework is grounded on open source tools for instrumenting, analyzing, and reporting spatio-temporal behaviors in webpages. We demonstrate our approach in practice over web accessibility standards posing challenges for automated verification.

Correct behavior of flight software against its requirements is a prime concern spanning its design, implementation, and operation. The emergence of “New Space” presents new challenges associated with small-scale missions which often involve open software frameworks, are developed by diverse teams, and employ rapid development methodologies which may not enjoy the rigorous quality assurance that institutional missions do. Hence, there is an overarching need to incor-porate contemporary engineering techniques and methods for checking requirement satisfaction for such flight software. To this end, this paper proposes GOP RIM E, designed to integrate goal monitoring within F’, a renowned software development framework developed by the Jet Propulsion Laboratory for embedded and spaceflight systems. GOPRIME consists of three phases: (i) a design phase, where annotations are used to align system-level objectives with architectural components; (ii) an implementation phase, where code generation tailored for the DSL of F’ is used to seamlessly automate the integration of goal monitoring functionality, and (iii) the operational phase, where the runtime state of annotated components is monitored, enabling evaluation of satisfaction of the overall goal model. We assess the development and operation overheads of instrumenting runtime goal monitoring over a characteristic case of a miniaturized satellite application.

Design by Contract represents an established, lightweight paradigm for engineering reliable and robust software systems by specifying verifiable expectations and obligations between software components. Due to its laborious nature, developers hardly adopt Design by Contract in practice. A plethora of research on (semi-)-automated inference to reduce the manual burden has not improved the adoption of so-called code contracts in practice. This paper examines the potential of Generative AI to automatically generate code contracts in terms of pre- and postconditions for any Java project without requiring any additional auxiliary artifact. To fine-tune two state-of-the-art Large Language Models, CodeT5 and CodeT5+, we derive a dataset of more than 14k Java methods comprising contracts in form of Java Modeling Language (JML) annotations, and train the models on the task of generating contracts. We examine the syntactic and semantic validity of the contracts generated for software projects not used in the fine-tuning and find that more than 95% of the generated contracts are syntactically correct and exhibit remarkably high completeness and semantic correctness. To this end, our fully automated method sets the stage for future research and eventual broader adoption of Design by Contract in software development practice.

Metamorphic testing involves reasoning on necessary properties that a program under test should exhibit regarding multiple input and output variables. A general approach consists of extracting metamorphic relations from auxiliary artifacts such as user manuals or documentation, a strategy particularly fitting to testing scientific software. However, such software typically has large input-output spaces, and the fundamental prerequisite – extracting variables of interest – is an arduous and non-scalable process when performed manually. To this end, we devise a workflow around an autoregressive transformer-based Large Language Model (LLM) towards the extraction of variables from user manuals of scientific software. Our end-to-end approach, besides a prompt specification consisting of few-shot examples by a human user, is fully automated, in contrast to current practice requiring human intervention. We showcase our LLM workflow over a real case, and compare variables extracted to ground truth manually labelled by experts. Our preliminary results show that our LLM-based workflow achieves an accuracy of 0.87, while successfully deriving 61.8% of variables as partial matches and 34.7% as exact matches.

Abstract Modelling the dynamics of a growing financial environment is a complex task that requires domain knowledge, expertise and access to heterogeneous information types. Such information can stem from several sources at different scales, complicating the task of forming a holistic impression of the financial landscape, especially in terms of the economical relationships between firms. Bringing this scattered information into a common context is, therefore, an essential step in the process of obtaining meaningful insights about the state of an economy. In this paper, we present Sabrina 2.0, a Visual Analytics (VA) approach for exploring financial data across different scales, from individual firms up to nation‐wide aggregate data. Our solution is coupled with a pipeline for the generation of firm‐to‐firm financial transaction networks, fusing information about individual firms with sector‐to‐sector transaction data and domain knowledge on macroscopic aspects of the economy. Each network can be created to have multiple instances to compare different scenarios. We collaborated with experts from finance and economy during the development of our VA solution, and evaluated our approach with seven domain experts across industry and academia through a qualitative insight‐based evaluation. The analysis shows how Sabrina 2.0 enables the generation of insights, and how the incorporation of transaction models assists users in their exploration of a national economy.

The communication of web services is typically organized through APIs, which rely on a common data model shared among system components. Over time, this data model must be changed in order to accommodate new or changing requirements, and the components including the data they are operating on must be migrated. In practice however, not all affected components can be migrated instantly and at the same time. A common approach is to plan data model changes in a backward compatible fashion, which causes serious maintenance problems and is a common cause of technical debt. We propose an alternative solution, using a translation layer serving as a round-trip migration service, responsible for the lossless translation of object-oriented data model instances of different versions. We present a framework which offers a version-aware interface definition language (IDL) for APIs, a typed JavaScript-based language using the IDL definition, and a run-time environment. From a methodological point of view, development is supported by a catalog which comprises a set of typical evolution scenarios along with corresponding round-trip migration strategies. We showcase the applicability of our approach via a case study of a real-world e-commerce web application, and evaluate correctness through automated testing.

With many applications across domains as diverse as logistics, healthcare, and agriculture, service robots are in increasingly high demand. Nevertheless, the designers of these robots often struggle with specifying their tasks in a way that is both human-understandable and sufficiently precise to enable automated verification and planning of robotic missions. Recent research has addressed this problem for the functional aspects of robotic missions through the use ofmission specification patterns. These patterns support the definition of robotic missions involving, for instance, the patrolling of a perimeter, the avoidance of unsafe locations within an area, or reacting to specific events. Our article introduces a catalog ofQUantitAtive RoboTic mission spEcificaTion patterns(QUARTET) that tackles the complementary and equally important challenge of specifying the reliability, performance, resource usage, and other key quantitative properties of robotic missions. Identified using a methodology that included the analysis of 73 research papers published in 17 leading software engineering and robotics venues between 2014–2021, our 22 QUARTET patterns are defined in a tool-supported domain-specific language. As such, QUARTET enables: (i) the precise definition of quantitative robotic-mission requirements and (ii) the translation of these requirements into probabilistic reward computation tree logic (PRCTL), supporting their formal verification and automated planning of robotic missions. We demonstrate the applicability of QUARTET by showing that it supports the specification of over 95% of the quantitative robotic mission requirements from a systematically selected set of recent research papers, of which 75% can be automatically translated into PRCTL for the purposes of verification through model checking and mission planning.

Analysis of data is the foundation of multiple scientific disciplines, manifesting in complex and diverse scientific data analysis workflows often involving exploratory analyses. Such analyses represent a particular case for traditional data engineering workflows, as results may be hard to interpret and judge whether they are correct or not, and where experimentation is a central theme. Oftentimes, there are certain aspects of a result which are suspicious and which should be further investigated to increase the trustworthiness of the workflow’s outcome. To this end, we advocate a semi-automated approach to reducing a workflow’s input data while preserving a specified outcome of interest, facilitating irregularity localization by narrowing down the search space for spotting corrupted input data or wrong assumptions made about it. We outline our vision on building engineering support for outcome-preserving input reduction within data analysis workflows, and report on preliminary results obtained from applying an early research prototype on a computational notebook taken from an online community of data scientists and machine learning practitioners.

Application development for the modern Web involves sophisticated engineering workflows which include user interface aspects. Those involve Web elements typically created with HTML/CSS markup and JavaScript-like languages, yielding Web documents. WebMonitor leverages requirements formally specified in a logic able to capture both the layout of visual components as well as how they change over time, as a user interacts with them. Then, requirements are verified upon arbitrary web pages, allowing for automated support for a wide set of use cases in interaction testing and simulation. We position WebMonitor within a developer workflow, where in case of a negative result, a visual counterexample is returned. The monitoring framework we present follows a black-box approach, and as such is independent of the underlying technologies a Web application may be developed with, as well as the browser and operating system used.

Edge computing offers the possibility of deploying applications at the edge of the network. To take advantage of available devices’ distributed resources, applications often are structured as microservices, often having stringent requirements of low latency and high availability. However, a decentralized edge system that the application may be intended for is characterized by high volatility, due to devices making up the system being unreliable or leaving the network unexpectedly. This makes application deployment and assurance that it will continue to operate under volatility challenging. We propose an adaptive framework capable of deploying and efficiently maintaining a microservice-based application at runtime, by tackling two intertwined problems: (i) finding a microservice placement across device hosts and (ii) deriving invocation paths that serve it. Our objective is to maintain correct functionality by satisfying given requirements in terms of end-to-end latency and availability, in a volatile edge environment. We evaluate our solution quantitatively by considering performance and failure recovery.

Satisfying the software requirements of emerging service-based Internet of Things (IoT) applications has become challenging for cloud-centric architectures, as applications demand fast response times and availability of computational resources closer to end-users. Meeting application demands must occur at runtime, facing uncertainty and in a decentralized manner, something that must be reflected in system deployment. We propose a decentralized resource management technique and accompanying technical framework for the deployment of service-based IoT applications at the edge. Faithful to services engineering, applications we consider are composed of interdependent tasks, which in the IoT setting may be concretized as containerized microservices or serverless functions. A deployment for an arbitrary application is found at runtime through satisfiability; the mapping produced is compliant with tasks’ individual resource requirements and latency constraints by construction. Our approach ensures seamless deployment at runtime, assuming no design-time knowledge of device resources or the current network topology. We evaluate the applicability and realizability of our technique over single-board computers as edge devices, particularly in the absence of cloud resources.

Complex distributed systems such as the ones induced by Internet of Things (IoT) deployments, are expected to operate in compliance to their requirements. This can be checked by inspecting events flowing throughout the system, typically originating from end-devices and reflecting arbitrary actions, changes in state or sensing. Such events typically reflect the behavior of the overall IoT system – they may indicate executions which satisfy or violate its requirements. This article presents a service-based software architecture and technical framework supporting runtime verification for widely deployed, volatile IoT systems. At the lowest level, systems we consider are comprised of resource-constrained devices connected over wide area networks generating events. In our approach, monitors are deployed on edge components, receiving events originating from end-devices or other edge nodes. Temporal logic properties expressing desired requirements are then evaluated on each edge monitor in a runtime fashion. The system exhibits decentralization since evaluation occurs locally on edge nodes, and verdicts possibly affecting satisfaction of properties on other edge nodes are propagated accordingly. This reduces dependence on cloud infrastructures for IoT data collection and centralized processing. We illustrate how specification and runtime verification can be achieved in practice on a characteristic case study of smart parking. Finally, we demonstrate the feasibility of our design over a testbed instantiation, whereupon we evaluate performance and capacity limits of different hardware classes under monitoring workloads of varying intensity using state-of-the-art LPWAN technology.

Complex distributed systems such as the ones induced by Internet of Things (IoT) deployments, are expected to operate in compliance to their requirements. This can be checked by inspecting events flowing throughout the system, typically originating from end-devices and reflecting arbitrary actions, changes in state or sensing. Such events typically reflect the behavior of the overall IoT system – they may indicate executions which satisfy or violate its requirements.

Engineering cyber-physical systems inhabiting contemporary urban spatial environments demands software engineering facilities to support design and operation. Tools and approaches in civil engineering and architectural informatics produce artifacts that are geometrical or geographical representations describing physical spaces. The models we consider conform to the CityGML standard; although relying on international standards and accessible in machine-readable formats, such physical space descriptions often lack semantic information that can be used to support analyses. In our context, analysis as commonly understood in software engineering refers to reasoning on properties of an abstracted model-in this case a city design. We support model-based development, firstly by providing a way to derive analyzable models from CityGML descriptions, and secondly, we ensure that changes performed are propagated correctly. Essentially, a digital twin of a city is kept synchronized, in both directions, with the information from the actual city. Specifically, our formal programming technique and accompanying technical framework assure that relevant information added, or changes applied to the domain (resp. analyzable) model are reflected back in the analyzable (resp. domain) model automatically and coherently. The technique developed is rooted in the theory of bidirectional transformations, which guarantees that synchronization between models is consistent and well behaved. Produced models can bootstrap graph-theoretic, spatial or dynamic analyses. We demonstrate that bidirectional transformations can be achieved in practice on real city models.

Recent advancements in information technology have ushered a new wave of systems integrating Internet technology with sensing, wireless communication, and computational resources over existing infrastructures. As a result, myriad complex, non-traditional Cyber-Physical Systems (CPS) have emerged, characterized by interaction among people, physical facilities, and embedded sensors and computers, all generating vast amounts of complex data. Such a case is encountered within a contemporary airport hall setting: passengers roaming, information systems governing various functions, and data being generated and processed by cameras, phones, sensors, and other Internet of Things technology. This setting has considerable potential of contributing to goals entertained by the CPS operators, such as airlines, airport operators/owners, technicians, users, and more. We model the airport setting as an instance of such a complex, data-intensive CPS where multiple actors and data sources interact, and generalize a methodology to support it and other similar systems. Furthermore, this article instantiates the methodology and pipeline for predictive analytics for passenger flow, as a characteristic manifestation of such systems requiring a tailored approach. Our methodology also draws from DataOps principles, using multi-modal and real-life data to predict the underlying distribution of the passenger flow on a flight-level basis (improving existing day-level predictions), anticipating when and how the passengers enter the airport and move through the check-in and baggage drop-off process. This allows to plan airport resources more efficiently while improving customer experience by avoiding passenger clumping at check-in and security. We demonstrate results obtained over a case from a major international airport in the Netherlands, improving up to 60% upon predictions of daily passenger flow currently in place.

Mobile and general-purpose robots increasingly support everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing complex behaviors known as missions. Recognizing this need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation or guiding implementation. For instance, the logical language LTL is commonly used by experts to specify missions as an input for planners, which synthesize a robot's required behavior. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems; each pattern details the usage intent, known uses, relationships to other patterns, and—most importantly—a template mission specification in temporal logic. Our tooling produces specifications expressed in the temporal logics LTL and CTL to be used by planners, simulators or model checkers. The patterns originate from 245 mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios defined with two well-known industrial partners developing human-size robots. We further validate our patterns’ correctness with simulators and two different types of real robots.

Systematic model-driven design and early validation enable engineers to verify that a reactive system does not violate its requirements before actually implementing it. Requirements may come from multiple stakeholders, who are often concerned with different facets - design typically involves different experts having different concerns and views of the system. Engineers start from a specification which may be sourced from some domain model, while validation is often done on state-transition structures that support model checking. Two computationally expensive steps may work against scalability: transformation from specification to state-transition structures, and model checking. We propose a technique that makes the former efficient and also makes the resulting transition systems small enough to be efficiently verified. The technique automatically projects the specification into submodels depending on a property sought to be evaluated, which captures some stakeholder's viewpoint. The resulting reactive system submodel is then transformed into a state-transition structure and verified. The technique achieves cone-of-influence reduction, by slicing at the specification model level. Submodels are analysis-equivalent to the corresponding full model. If stakeholders propose a change to a submodel based on their own view, changes are automatically propagated to the specification model and other views affected. Automated reflection is achieved thanks to bidirectional model transformations, ensuring correctness. We cast our proposal in the context of graph-based reactive systems whose dynamics is described by rewriting rules. We demonstrate our view-based framework in practice on a case study within cyber-physical systems.

Internet-enabled devices operating in the physical world are increasingly integrated in modern distributed systems. We focus on systems where the dynamics of spatial distribution is crucial; in such cases, devices may need to carry out complex computations (e.g., analyses) to check satisfaction of spatial requirements. The requirements are partly global—as the overall system should achieve certain goals—and partly individual, as each entity may have different goals. Assurance may be achieved by keeping a model of the system at runtime, monitoring events that lead to changes in the spatial environment, and performing requirements analysis. However, computationally intensive runtime spatial analysis cannot be supported by resource-constrained devices and may be offloaded to the cloud. In such a scenario, multiple challenges arise regarding resource allocation, cost, performance, among other dimensions. In particular, when the workload is unknown at the system’s design time, it may be difficult to guarantee application-service-level agreements, e.g., on response times. To address and reason on these challenges, we first instantiate complex computations as microservices and integrate them to an IoT-cloud architecture. Then, we propose alternative cloud deployments for such an architecture—based on virtual machines, containers, and the recent Functions-as-a-Service paradigm. Finally, we assess the feasibility and tradeoffs of the different deployments in terms of scalability, performance, cost, resource utilization, and more. We adopt a workload scenario from a known dataset of taxis roaming in Beijing, and we derive other workloads to represent unexpected request peaks and troughs. The approach may be replicated in the design process of similar classes of spatially distributed IoT systems.

Internet of Things (IoT) systems open up massive versatility and opportunity to our world. Providing solutions for smart cities, healthcare, energy, and mobility, such systems increasingly permeate critical aspects of human activity. In a flourish of growth, these complex systems run software, are dynamic, without stable spatial and temporal boundaries, and involve mostly independent software components with different lifespans and evolution models. IoT systems provide data-centric, device-centric and service-centric functionalities that are subject to continuous disruption, under limitations such as resource-constrained devices, platforms heterogeneity, deployment in adverse environments and administrative domains. As these systems evolve and gain complexity, resilience becomes a crucial system property. Bolstering resilience entails understanding and systematically managing dynamic behavior and decentralizing operations. We advocate that to systematically engineer resilience in IoT systems, a complete rethink is necessary regarding their design and operation. In this paradigm shift, systems demand conceptual frameworks, techniques, and mathematically-backed formalisms to treat change and achieve decentralization. We outline a vision for addressing fundamental challenges that software engineering and distributed systems research encounters when building resilient IoT systems. Within a roadmap, we identify techniques and methods that can be leveraged to maintain resilience in the face of disruption, especially in the absence of central control and persistently at the system's runtime.

Edge computing has been recently introduced as an intermediary between Internet of Things (IoT) deployments and the cloud, providing data or control facilities to participating IoT devices. This includes actively supporting IoT resource discovery, something particularly pertinent when building large-scale, distributed and heterogeneous IoT systems. Moreover, edge devices supporting resource discovery are required to meet the stringent requirements prevalent in IoT systems including high availability, low-latency, and privacy. To this end, we present a resource discovery platform for IoT resources situated at the edge of the network. Our approach aims at providing a seamless discovery process that is able to (i) extend the covered area by deploying additional edge nodes and (ii) assist in the development of new IoT applications that target already available resources. Within our proposed platform, devices located in a certain proximity connect and form an edge-to-edge network that we call an edge neighborhood - our edge-to-edge metadata replication platform enables participating devices to discover available resources. Our solution is characterized by absence of centralization, as edge nodes exchange metadata about available resources within their scope in a peer-to-peer manner.

Technological advances enable new kinds of smart environments exhibiting complex behaviors; smart cities are a notable example. Smart functionalities heavily depend on space and need to be aware of entities typically found in the spatial domain, e.g. roads, intersections or buildings in a smart city. We advocate a model-based development, where the model of physical space, coming from the architecture and civil engineering disciplines, is transformed into an analyzable model upon which smart functionalities can be embedded. Such models can then be formally analyzed to assess a composite system design. We focus on how a model of physical space specified in the CityGML standard language can be transformed into a model amenable to analysis and how the two models can be automatically kept in sync after possible changes. This approach is essential to guarantee safe model-driven development of composite systems inhabiting physical spaces. We showcase transformations of real CityGML models in the context of scenarios concerning both design time and runtime analysis of space-dependent systems.

Comprehensive privacy mechanisms are essential in the pervasive internet-of-things systems of today, which are comprised of multiple distributed devices and diverse software stacks, while located in different legal or administrative domains. In such systems, often consisting of resource-constrained devices, guarantees of correctness and conformance to privacy policies is required, while data need to be synchronized among different software components. Motivated by the "data protection by design and by default" principle, we propose a technical framework to support data synchronization among edge components tailored for pervasive IoT applications. Our privacy-driven synchronization approach is based on a generically applicable privacy model and able to capture roles and permissions, actions on data, conditions and obligations that arise in privacy requirements. For automated and correct reflection of synchronized data among components, we adopt bidirectional transformations, a mechanism where synchronization between models, consistency, and well-behavedness are formally guaranteed. Thus, automatically generated privacy-aware data transformations are correct by construction. We evaluate POET, our framework and accompanying tool with a case study on medical information privacy and demonstrate its performance in resource-constrained edge devices.

Software components within heterogeneous devices of the Internet of Things (IoT) systems use resources representing various computational capabilities, including sensing or actuation end points. However, components do not live in isolation and must be able to coordinate with others to fulfill their goals. Satisfaction of requirements-capturing their goals-must persist in environments that are changing, unpredictable, and potentially unknown at system design time. Edge computers placed near IoT devices can be leveraged for this sort of control-providing resource management for end devices within their operational context. We propose a methodology and technical framework for engineering resource coordination at runtime, tailored for the decentralized, pervasive systems of today. Our approach represents a paradigm shift in marrying distributed systems and formal aspects of software engineering. We adopt goal modeling to capture objectives within the system and use bounded model checking as the foundational technique to compute coordination plans that satisfy device goals. This occurs opportunistically at runtime without any knowledge about the operational status or presence of resources, but always in accordance with the edge's own goals. Our technical framework exhibits dependability guarantees regarding optimality and correctness of generated plans. We evaluate the resource coordination performance and its feasibility on low-powered ARM-based edge devices.

Ubiquitous computing is resulting in a proliferation of cyber-physical systems that host or manage valuable physical and digital assets. These assets can be harmed by malicious agents through both cyber-enabled or physically-enabled attacks, particularly ones that exploit the often ignored interplay between the cyber and physical world. The explicit representation of spatial topology is key to supporting adaptive security policies. In this paper we explore the use of Bigraphical Reactive Systems to model the topology of cyber and physical spaces and their dynamics. We utilise such models to perform speculative threat analysis through model checking to reason about the consequences of the evolution of topological configurations on the satisfaction of security requirements. We further propose an automatic planning technique to identify an adaptation strategy enacting security policies at runtime to prevent, circumvent, or mitigate possible security requirements violations. We evaluate our approach using a case study concerned with countering insider threats in a building automation system.

We increasingly live in cyber-physical spaces -- spaces that are both physical and digital, and where the two aspects are intertwined. Such spaces are highly dynamic and typically undergo continuous change. Software engineering can have a profound impact in this domain, by defining suitable modeling and specification notations as well as supporting design-time formal verification. In this paper, we present a methodology and a technical framework which support modeling of evolving cyber-physical spaces and reasoning about their spatio-temporal properties. We utilize a discrete, graph-based formalism for modeling cyber-physical spaces as well as primitives of change, giving rise to a reactive system consisting of rewriting rules with both local and global application conditions. Formal reasoning facilities are implemented adopting logic-based specification of properties and according model checking procedures, in both spatial and temporal fragments. We evaluate our approach using a case study of a disaster scenario in a smart city.

Managing, configuring and deploying complex applications in the cloud are emerging problems in contemporary cloud computing. Cloud workload specifications, as portable abstractions of cloud computations, are an important means to deal with these problems on an architectural level. They focus on defining the components of an application and their structural relations, workflows regarding their initialization and management, along with configuration and artifacts required for application operation. The prevalence of cloud computing drives demand for applications that rely on systematic engineering and smell-free architectures, thus quality assurance techniques for cloud workload specifications are strongly required. In particular, cloud workload specifications exhibit characteristics of software architectures such as patterns or anti-patterns which state desired or undesired quality aspects. To facilitate formal reasoning about latent qualities of a workload design, we propose a static bigraphical semantics for the modeling language defined by the emerging Topology and Orchestration Specification for Cloud Applications (TOSCA) standard. Thereupon, we illustrate how to check for the presence (absence) of (anti-)patterns expressed as logical formulae over bigraphical predicates.

This paper presents Ariadne, a tool for engineering topology aware adaptive security for cyber-physical systems. It allows security software engineers to model security requirements together with the topology of the operational environment. This model is then used at runtime to perform speculative threat analysis to reason about the consequences that topological changes arising from the movement of agents and assets can have on the satisfaction of security requirements. Our tool also identifies an adaptation strategy that applies security controls when necessary to prevent potential security requirements violations.

Adaptive security systems aim to protect critical assets in the face of changes in their operational environment. We have argued that incorporating an explicit representation of the environment's topology enables reasoning on the location of assets being protected and the proximity of potentially harmful agents. This paper proposes to engineer topology aware adaptive security systems by identifying violations of security requirements that may be caused by topological changes, and selecting a set of security controls that prevent such violations. Our approach focuses on physical topologies; it maintains at runtime a live representation of the topology which is updated when assets or agents move, or when the structure of the physical space is altered. When the topology changes, we look ahead at a subset of the future system states. These states are reachable when the agents move within the physical space. If security requirements can be violated in future system states, a configuration of security controls is proactively applied to prevent the system from reaching those states. Thus, the system continuously adapts to topological stimuli, while maintaining requirements satisfaction. Security requirements are formally expressed using a propositional temporal logic, encoding spatial properties in Computation Tree Logic (CTL). The Ambient Calculus is used to represent the topology of the operational environment - including location of assets and agents - as well as to identify future system states that are reachable from the current one. The approach is demonstrated and evaluated using a substantive example concerned with physical access control.