This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behaviour, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalise in Rocq. This method can be seen as a specialised induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviour by standard techniques.

The advent of digital twins gives us an opportunity to reflect on the relationship between models and modelled systems. We may think of digital twins not merely as models, but as systems for model management, integration, and composition. In fact, digital twins are model-centric systems that maintain a two-way connection between an ecosystem of models and the modelled system, realised through streams of observations and streams of interventions. This connection introduces agility as the digital twin can typically both adapt its models on-the-fly to changes in a modelled system and influence the modelled system’s behaviour. In this paper, we discuss key concepts of digital twins from a formal methods perspective and suggest opportunities and challenges for formal methods in digital twin systems. In particular, we consider how formal techniques can be integral to the digital twin, both in terms of digital twin technology and in terms of digital twin models, as well as notions of correctness for the digital twin itself.

With the advent of AI-driven applications, testing faces new challenges when it comes to the integration of software with AI components. We present a novel testing approach to tackle the integration of software with symbolic AI in the form of knowledge graphs (KG). As the KG is expected to change during the run- and lifetime of the software, we must ensure the robustness of the system w.r.t. changes in the KG. Starting with a single KG, we mutate its content and test the unchanged software with the original test oracle. To address the specific challenges of KGs, we introduce two additional concepts. First, as generic mutations on single triples are too fine-grained to reliably generate a KG describing a different, consistent KG, we introduce domain-specific mutation operators that manipulate subgraphs in a domain-adherent way. Second, we need to specify those parts of the knowledge graph that the software relies on for correctness. We introduce the notion of a robustness mask to describe shapes in the graph to which the mutant must conform. We evaluate our approach on two software applications from the robotic and simulation domain that tightly integrate with their respective KG, as well as three OWL reasoners, where we found several previously unknown bugs.

Abstract Self-adaptive systems can be realised as layered systems with a feedback loop: a managing system monitors a managed system, updates an internal model, and adjusts the managed system by means of controllers to maintain given requirements. For example, a digital twin coupled with its physical twin constitute such a self-adaptive system. As the managed system shifts between different stages in its lifecycle, these requirements, as well as the associated analysers and controllers, may need to change. The exact triggers for such shifts in a managed system are often hard to predict: they may be difficult to describe or even unknown. However, the shifts can generally be observed once they have occurred, in terms of changes in the system behaviour. This paper proposes an automated method for self-adaptation in self-adaptive systems to address shifts between lifecycle stages in a managed system. Our method is based on declarative descriptions of lifecycle stages for assets in a managed system and their associated counterparts in the managing system. Declarative lifecycle management provides a high-level, flexible method of self-adaptation for self-adaptive systems to reflect disruptive shifts between stages in a managed system.

With the servitization of business, understanding how users experience services becomes a crucial success factor for companies. Therefore, there is a need to include feedback from user experiences in the software engineering process. Behavioral models of user journeys, describing how users experience their interaction with a service, can provide insights and potentially improve services. In this paper, we investigate techniques that allow the automatic generation of behavioral models from user interactions with a service, recorded in an event log. We first compare two established techniques that generate behavioral models from a given event log: automata learning and process mining. Afterward, we present a novel, hybrid method that combines both automata learning and process mining methods to overcome their limitations. For the existing techniques, we present methods to learn models of user journeys and evaluate the accuracy of the resulting models. We then compare these techniques with our novel method for the automatic extraction of user journey models from the event logs of digital services. We assess the practical applicability of all techniques by evaluating real-world applications. Our results show that process mining techniques rely on expert knowledge, while automata learning techniques depend on the distribution of events in the given event log. We further show that the proposed hybrid technique combines the strengths of both process mining and automata learning, automatically selecting the best method and parameter settings for a given event log to learn very accurate models.

Abstract Tabular reinforcement learning methods cannot operate directly on continuous state spaces. One solution to this problem is to partition the state space. A good partitioning enables generalization during learning and more efficient exploitation of prior experiences. Consequently, the learning process becomes faster and produces more reliable policies. However, partitioning introduces approximation, which is particularly harmful in the presence of nonlinear relations between state components. An ideal partition should be as coarse as possible, while capturing the key structure of the state space for the given problem. This work extracts partitions from the environment dynamics by symbolic execution. We show that symbolic partitioning improves state space coverage with respect to environmental behavior and allows reinforcement learning to perform better for sparse rewards. We evaluate symbolic state space partitioning with respect to precision, scalability, learning agent performance and state space coverage for the learned policies.

Counterfactuals are widely used in AI to explain how minimal changes to a model’s input can lead to a different output. However, established methods for computing counterfactuals typically focus on one-step decision-making, and are not directly applicable to sequential decision-making tasks. This paper fills this gap by introducing counterfactual strategies for Markov Decision Processes (MDPs). During MDP execution, a strategy decides which of the enabled actions (with known probabilistic effects) to execute next. Given an initial strategy that reaches an undesired outcome with a probability above some limit, we identify minimal changes to the initial strategy to reduce that probability below the limit. We encode such counterfactual strategies as solutions to non-linear optimization problems, and further extend our encoding to synthesize diverse counterfactual strategies. We evaluate our approach on four real-world datasets and demonstrate its practical viability in sophisticated sequential decision-making tasks.

Improved autonomy in robotic systems is needed for innovation in, e.g., the marine sector. Autonomous robots that are let loose in hazardous environments, such as underwater, need to handle uncertainties that stem from both their environment and internal state. While self-adaptation is crucial to cope with these uncertainties, bad decisions may cause the robot to get lost or even to cause severe environmental damage. Autonomous, self-adaptive robots that operate in uncontrolled environments full of uncertainties need to be reliable! Since these uncertainties are hard to replicate in test deployments, we need methods to formally analyse self-adaptive robots operating in uncontrolled environments. In this article, we show how feature-oriented techniques can be used to formally model and analyse self-adaptive robotic systems in the presence of such uncertainties. Self-adaptive systems can be organised as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of an Autonomous Underwater Vehicle (AUV) for pipeline inspection, in which the managed subsystem of the AUV is modelled as a family of systems, where each family member corresponds to a valid configuration of the AUV which can be seen as an operating mode of the AUV’s behaviour. The managing subsystem of the AUV is modelled as a control layer that is capable of dynamically switching between such valid configurations, depending on both environmental and internal uncertainties. These uncertainties are captured in a probabilistic and highly configurable model. Our modelling approach allows us to exploit powerful formal methods for feature-oriented systems, which we illustrate by analysing safety properties, energy consumption, and multi-objective properties, as well as performing parameter synthesis to analyse to what extent environmental conditions affect the AUV. The case study is realised in the probabilistic feature-oriented modelling language and verification tool ProFeat, and in particular exploits family-based probabilistic and parametric model checking.

Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems (SASs) can be realised as two-layered systems, introducing a separation of concerns between the domain-specific functionalities of the system (the managed subsystem) and the adaptation logic (the managing subsystem), i.e., introducing an external feedback loop for managing adaptation in the system. We present an approach to model SASs as dynamic software product lines (SPLs) and leverage existing approaches to SPL-based analysis for the analysis of SASs. To do so, the functionalities of the SAS are modelled in a feature model, capturing the SAS’s variability. This allows us to model the managed subsystem of the SAS as a family of systems, where each family member corresponds to a valid feature configuration of the SAS. Thus, the managed subsystem of an SAS is modelled as an SPL model; more precisely, a probabilistic featured transition system. The managing subsystem of an SAS is modelled as a control layer capable of dynamically switching between these valid configurations, depending on both environmental and internal conditions. We demonstrate the approach on a small-scale evaluation of a self-adaptive autonomous underwater vehicle used for pipeline inspection, which we model and analyse with the feature-aware probabilistic model checker ProFeat. The approach allows us to analyse probabilistic reward and safety properties for the SAS, as well as the correctness of its adaptation logic. • Dynamic software product lines used to model self-adaptive systems. • Family-based analysis used for formal verification of self-adaptive systems. • A case study from the underwater robotics domain to exemplify the approach. • Maintaining separation of concerns between the two layers of a self-adaptive system.

Self-adaptation, meant to increase reliability, is a crucial feature of cyber-physical systems operating in uncertain physical environments. Ensuring safety properties of self-adaptive systems is of utter importance, especially when operating in remote environments where communication with a human operator is limited, like under water or in space. This paper presents a software model that allows the analysis of one such self-adaptive system, a configurable underwater robot used for pipeline inspection, by means of the probabilistic model checker ProFeat. Furthermore, it shows that the configurable software model is easily extensible to further, possibly more complex use cases and analyses.

Symbolic execution is a program analysis technique to systematically explore all possible paths through a program. The technique can be formally explained by means of small-step transition systems that update symbolic states and compute a precondition corresponding to the taken execution path. In stateful transition systems behavior may depend on previous transitions, which complicates compositional reasoning about programs. To enable compositonal reasoning this paper defines a denotational semantics for symbolic execution. The proposed semantics views a program as a set of traces, each of which has a corresponding substitution — the composition of all its assignments — and a corresponding path condition — the conjunction of all its Boolean tests under appropriate substitution. We prove correspondence between the symbolic denotational semantics and a concrete semantics. We argue that the symbolic denotational semantics is a very natural framework to reason about symbolic execution, and use it to prove that symbolic execution computes (weakest) preconditions. We provide mechanizations in Coq for the main results.

Abstract Industry is shifting towards service-based business models, for which user satisfaction is crucial. User satisfaction can be analyzed with user journeys, which model services from the user’s perspective. Today, these models are created manually and lack both formalization and tool-supported analysis. This limits their applicability to complex services with many users. Our goal is to overcome these limitations by automated model generation and formal analyses, enabling the analysis of user journeys for complex services and thousands of users. In this paper, we use stochastic games to model and analyze user journeys. Stochastic games can be automatically constructed from event logs and model checked to, e.g., identify interactions that most effectively help users reach their goal. Since the learned models may get large, we use property-preserving model reduction to visualize users’ pain points to convey information to business stakeholders. The applicability of the proposed method is here demonstrated on two complementary case studies.

Autonomous Underwater Vehicles (AUVs) need to operate for days without human intervention and thus must be able to do efficient and reliable task planning. Unfortunately, efficient task planning requires deliberately abstract domain models (for scalability reasons), which in practice leads to plans that might be unreliable or under performing in practice. An optimal abstract plan may turn out suboptimal or unreliable during physical execution. To overcome this, we introduce a method that first generates a selection of diverse high-level plans and then assesses them in a low-level simulation to select the optimal and most reliable candidate. We evaluate the method using a realistic underwater robot simulation, estimating the risk metrics for different scenarios, demonstrating feasibility and effectiveness of the approach.

With the advent of AI-driven applications, testing faces new challenges when it comes to the integration of software with AI components. We present a novel testing approach to tackle the integration of software with symbolic AI in the form of knowledge graphs (KG). As the KG is expected to change during the run- and lifetime of the software, we must ensure the robustness of the system w.r.t. changes in the KG. Starting with a singular KG, we mutate its content and test the unchanged software with the original test oracle. To address the specific challenges of KGs, we introduce two additional concepts. First, as generic mutations on single triples are too fine-grained to reliably generate a KG describing a different, consistent KG, we employ domain-specific mutation operators, that manipulate subgraphs in a domain-adherent way. Second, we need to specify those parts of the knowledge that the software relies on for correctness. We introduce the notion of a robustness mask as shapes in the graph that the mutant must conform to. We evaluate our approach on two software applications from the robotic and simulation domain that tightly integrate with their respective KG.

Abstract The servitization of business is moving industry to business models driven by customer demand. Customer satisfaction is connected with financial rewards, forcing companies to invest in their users’ experience. User journeys describe how users maneuver through a service. Today, user journeys are typically modeled graphically, and lack formalization and analysis support. This paper proposes a formalization of user journeys as weighted games between the user and the service provider and a systematic data-driven method to derive these user journey games from system logs, using process mining techniques. As the derived games may contain cycles, we define an algorithm to transform user journeys games with cycles into acyclic weighted games, which can be model checked using "Image missing" to uncover potential challenges in a company’s interactions with its users and derive company strategies to guide users through their journeys. Finally, we propose a user journey sliding-window analysis to detect changes in the user journey over time by model checking a sequence of generated games. Our analysis pipeline has been evaluated on an industrial case study; it revealed design challenges within the studied service and could be used to derive actionable recommendations for improvement.

This article addresses the long-standing problem of program correctness for programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level models expressed as transition systems. The implementation language underlying the method is based on the concurrency model of actors and active objects. The method defines program correctness in terms of a simulation relation between the transition system that specifies the program semantics of the parallel program and the transition system that is described by the correctness specification. The simulation relation itself abstracts from the fine-grained interleaving of parallel processes by exploiting a global confluence property of the concurrency model of the implementation language considered in this article. As a proof of concept, we apply our method to the correctness of a parallel simulator of multicore memory systems.

Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used in deductive verification and formal specification of concurrent programs. Our semantics separates local evaluation of expressions and statements performed in an abstract, symbolic environment from their composition into global computations, at which point they are concretised. This makes incremental addition of new language concepts possible, without the need to revise the framework. The basis is a generalisation of the notion of a program trace as a sequence of evolving states that we enrich with event descriptors and trailing continuation markers. This allows to postpone scheduling constraints from the level of local evaluation to the global composition stage, where well-formedness predicates over the event structure declaratively characterise a wide range of concurrency models. We also illustrate how a sound program logic and calculus can be defined for this semantics.

Once deployed in the real world, autonomous underwater vehicles (AUVs) are out of reach for human supervision yet need to take decisions to adapt to unstable and unpredictable environments. To facilitate research on self-adaptive AUVs, this paper presents SUAVE, an exemplar for two-layered system-level adaptation of AUVs, which clearly separates the application and self-adaptation concerns. The exemplar focuses on a mission for underwater pipeline inspection by a single AUV, implemented as a ROS 2-based system. This mission must be completed while simultaneously accounting for uncertainties such as thruster failures and unfavorable environmental conditions. The paper discusses how SUAVE can be used with different self-adaptation frameworks, illustrated by an experiment using the Metacontrol framework to compare AUV behavior with and without self-adaptation. The experiment shows that the use of Metacontrol to adapt the AUV during its mission improves its performance when measured by the overall time taken to complete the mission or the length of the inspected pipeline.

Cloud computing has radically changed the way organizations operate their Software by allowing them to achieve high availability of services at affordable cost. Containerized microservices is an enabling technology for this change, and advanced container orchestration platforms such as Kubernetes are used for service management. Despite the flourishing ecosystem of monitoring tools for such orchestration platforms, service management is still mainly a manual effort. The modeling of cloud computing systems is an essential step towards automatic management, but the modeling of cloud systems of such complexity remains challenging and, as yet, unaddressed. In fact modeling resource consumption will be a key to comparing the outcome of possible deployment scenarios. This paper considers how to derive resource models for cloud systems empirically. We do so based on models of deployed services in a formal modeling language with explicit CPU and memory resources; once the adherence to the real system is good enough, formal properties can be verified in the model. Targeting a likely microservices application, we present a model of Kubernetes developed in Real-Time ABS. We report on leveraging data collected empirically from small deployments to simulate the execution of higher intensity scenarios on larger deployments. We discuss the challenges and limitations that arise from this approach, and identify constraints under which we obtain satisfactory accuracy.

The development process for reinforcement learning applications is still exploratory rather than systematic. This exploratory nature reduces reuse of specifications between applications and increases the chances of introducing programming errors. This paper takes a step towards systematizing the development of reinforcement learning applications. We introduce a formal specification of reinforcement learning problems and algorithms, with a particular focus on temporal difference methods and their definitions in backup diagrams. We further develop a test harness for a large class of reinforcement learning applications based on temporal difference learning, including SARSA and Q-learning. The entire development is rooted in functional programming methods; starting with pure specifications and denotational semantics, ending with property-based testing and using compositional interpreters for a domain-specific term language as a test oracle for concrete implementations. We demonstrate the usefulness of this testing method on a number of examples, and evaluate with mutation testing. We show that our test suite is effective in killing mutants (90% mutants killed for 75% of subject agents). More importantly, almost half of all mutants are killed by generic write-once-use-everywhere tests that apply to any reinforcement learning problem modeled using our library, without any additional effort from the programmer.

Autonomous robots combine skills to form increasingly complex behaviors, called missions. While skills are often programmed at a relatively low abstraction level, their coordination is architecturally separated and often expressed in higher-level languages or frameworks. State machines have been the go-to language to model behavior for decades, but recently, behavior trees have gained attention among roboticists. Originally designed to model autonomous actors in computer games, behavior trees offer an extensible tree-based representation of missions and are claimed to support modular design and code reuse. Although several implementations of behavior trees are in use, little is known about their usage and scope in the real world. How do concepts offered by behavior trees relate to traditional languages, such as state machines? How are concepts in behavior trees and state machines used in actual applications? This paper is a study of the key language concepts in behavior trees as realized in domain-specific languages (DSLs), internal and external DSLs offered as libraries, and their use in open-source robotic applications supported by the Robot Operating System (ROS). We analyze behavior-tree DSLs and compare them to the standard language for behavior models in robotics: state machines. We identify DSLs for both behavior-modeling languages, and we analyze five in-depth. We mine open-source repositories for robotic applications that use the analyzed DSLs and analyze their usage. We identify similarities between behavior trees and state machines in terms of language design and the concepts offered to accommodate the needs of the robotics domain. We observed that the usage of behavior-tree DSLs in open-source projects is increasing rapidly. We observed similar usage patterns at model structure and at code reuse in the behavior-tree and state-machine models within the mined open-source projects. We contribute all extracted models as a dataset, hoping to inspire the community to use and further develop behavior trees, associated tools, and analysis techniques.

The General Data Protection Regulation (GDPR) regulates the handling of personal data, including that personal data may be collected and stored only with the data subject's consent, that data is used only for the explicit purposes for which it is collected, and that is deleted after the purposes are served. We propose a programming language called DPL (Data Protection Language) with constructs for enforcing these central GDPR requirements and provide the language's runtime operational semantics. DPL is designed so that GDPR violations cannot occur: potential violations instead result in runtime errors. Moreover, DPL provides constructs to perform privacy-relevant checks, which enable programmers to avoid these errors. Finally, we formalize DPL in Maude, yielding an environment for program simulation, and verify our claims that DPL programs cannot result in privacy violations.

ABS is a language for behavioral modeling of distributed, time- and resource-sensitive communicating systems. ABS is based on an executable actor-based semantics with asynchronous method calls, with method call results being delivered via future variables. Data is modeled via a functional, side-effect-free layer of algebraic data types and parametric functions. Actor behavior is expressed in a sequential, imperative way, with explicit suspension points for in-actor cooperative scheduling. A declarative time and resource model allows modeling of time-sensitive actor behavior in a compositional way. A software product line language layer implements model variability via code deltas and feature models. This paper describes the toolchain that makes it possible to simulate ABS models, and lists the most important case studies done with ABS.

Non-determinism in a concurrent or distributed setting may lead to many different runs or executions of a program. This paper presents a method to reproduce a specific run for non-deterministic actor or active object systems. The method is based on recording traces of events reflecting local transitions at so-called stable states during execution; i.e., states in which local execution depends on interaction with the environment. The paper formalizes trace recording and replay for a basic active object language, to show that such local traces suffice to obtain global reproducibility of runs; during replay different objects may operate fairly independently of each other and in parallel, yet a program under replay has guaranteed deterministic outcome. We then show that the method extends to the other forms of non-determinism as found in richer active object languages. Following the proposed method, we have implemented a tool to record and replay runs, and to visualize the communication and scheduling decisions of a recorded run, for Real-Time ABS, a formally defined, rich active object language for modeling timed, resource-aware behavior in distributed systems.

Highly-configurable software systems can have thousands of interdependent configuration options across different subsystems. In the resulting configuration space, discovering a valid product configuration for some selected options can be complex and error prone. The configuration space can be organized using a feature model, fragmented into smaller interdependent feature models reflecting the configuration options of each subsystem.

Autonomous robots combine a variety of skills to form increasingly complex behaviors called missions. While the skills are often programmed at a relatively low level of abstraction, their coordination is architecturally separated and often expressed in higher-level languages or frameworks. Recently, the language of Behavior Trees gained attention among roboticists for this reason. Originally designed for computer games to model autonomous actors, Behavior Trees offer an extensible tree-based representation of missions. However, even though, several implementations of the language are in use, little is known about its usage and scope in the real world. How do behavior trees relate to traditional languages for describing behavior? How are behavior tree concepts used in applications? What are the benefits of using them?

Concurrent programs often make use of futures, handles to the results of asynchronous operations. Futures provide means to communicate not yet computed results, and simplify the implementation of operations that synchronise on the result of such asynchronous operations. Futures can be characterised as implicit or explicit, depending on the typing discipline used to type them. Current future implementations suffer from "future proliferation", either at the type-level or at run-time. The former adds future type wrappers, which hinders subtype polymorphism and exposes the client to the internal asynchronous communication architecture. The latter increases latency, by traversing nested future structures at run-time. Many languages suffer both kinds. Previous work offer partial solutions to the future proliferation problems; in this paper we show how these solutions can be integrated in an elegant and coherent way, which is more expressive than either system in isolation. We describe our proposal formally, and state and prove its key properties, in two related calculi, based on the two possible families of future constructs (data-flow futures and control-flow futures). The former relies on static type information to avoid unwanted future creation, and the latter uses an algebraic data type with dynamic checks. We also discuss how to implement our new system efficiently.

This paper describes the development of a parallel simulator of a multicore memory system from a model formalized as a structural operational semantics (SOS). Our implementation uses the Abstract Behavioral Specification (ABS) language, an executable, active object modelling language with a formal semantics, targeting distributed systems. We develop general design patterns in ABS for implementing SOS, and describe their application to the SOS model of multicore memory systems. We show how these patterns allow a formal correctness proof that the implementation simulates the formal operational model and discuss further parallelization and fairness of the simulator.

As more and more devices connect to Internet of Things, unbounded streams of data will be generated, which have to be processed "on the fly" in order to trigger automated actions and deliver real-time services. Spark Streaming is a popular realtime stream processing framework. To make efficient use of Spark Streaming and achieve stable stream processing, it requires a careful interplay between different parameter configurations. Mistakes may lead to significant resource overprovisioning and bad performance. To alleviate such issues, this paper develops an executable and configurable model named SSP (stands for Spark Streaming Processing) to model and simulate Spark Streaming. SSP is written in ABS, which is a formal, executable, and object-oriented language for modeling distributed systems by means of concurrent object groups. SSP allows users to rapidly evaluate and compare different parameter configurations without deploying their applications on a cluster/cloud. The simulation results show that SSP is able to mimic Spark Streaming in different scenarios.

This article presents parallel cost analysis , a static cost analysis targeting to over-approximate the cost of parallel execution in distributed systems. In contrast to the standard notion of serial cost , parallel cost captures the cost of synchronized tasks executing in parallel by exploiting the true concurrency available in the execution model of distributed processing. True concurrency is challenging for static cost analysis, because the parallelism between tasks needs to be soundly inferred, and the waiting and idle processor times at the different locations need to be accounted for. Parallel cost analysis works in three phases: (1) it performs a block-level analysis to estimate the serial costs of the blocks between synchronization points in the program; (2) it then constructs a distributed flow graph (DFG) to capture the parallelism, the waiting, and idle times at the locations of the distributed system; and (3) the parallel cost can finally be obtained as the path of maximal cost in the DFG. We prove the correctness of the proposed parallel cost analysis, and provide a prototype implementation to perform an experimental evaluation of the accuracy and feasibility of the proposed analysis.

No abstract available.

Abstract Traits have been proposed as a more flexible mechanism than class inheritance for structuring code in object-oriented programming, to achieve fine-grained code reuse. A trait originally developed for one purpose can be adapted and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. So far, work on formally establishing properties of trait-based programs has mostly concentrated on type systems. This paper presents the first deductive proof system for a trait-based object-oriented language. If a specification of a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. However, imposing such a restriction may in many cases unnecessarily limit traits as a mechanism for flexible code reuse. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in anincrementalway which does not violate established proofs. We formalize and show the soundness of the proof system.

Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specifications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specifications in a delta module describe changes to previous specifications. Our approach allows each delta module to be verified in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specifications of this product variant.

Traits have been proposed as a more flexible mechanism for code structuring in object-oriented programming than class inheritance, for achieving fine-grained code reuse. A trait originally developed for one purpose can be modified and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. However, work on formally establishing properties of trait-based programs has so far mostly concentrated on type systems. This paper proposes the first deductive proof system for a trait-based object-oriented language. If a specification for a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in an incremental way which does not violate established proofs. We formalize and show the soundness of the proof system.

Wireless sensor networks consist of resource constrained nodes, especially with respect to power resources. In many cases, the replacement of a dead node is difficult and costly, e.g. an implanted node in the human body. Our main goal in this paper is reducing the total power consumption of the network. For this purpose, we consider the cooperation of nodes in data transmission in terms of a group, since the major consumer of power is the data transmission process. A mobile node may move to a new location, in which it is desirable for the node to join a group. In this paper, we propose an algorithm for nodes to choose the best group in their signal range, using coalitional game theory to determine what is beneficial in terms of power consumption. The protocol is formalized in rewriting logic, implemented in the Maude tool, and validated by means of Maude's model exploration facilities. Simulation-based tools are in general not able to prove the protocol. However, by using Maude, we prove the correctness of our proposed protocol, by searching for failures of the protocol, through all possible behaviors of sensors. These searches prove that grouping nodes is done correctly in all reachable states from a set of initial states of the model. In addition, we simulate our model in order to quantitatively analyze the efficiency of the proposed protocol. The results show significant improvements in power efficiency.

Convenience in specification and possibility for formal analysis are, to some extent, exclusive aspects of system specification. This paper describes an approach that emphasizes both aspects, by combining UML with a language for observable behavior of interfaces, OUN. These are complementary in the sense that one is graphical and semi-formal while the other is textual and formal. The approach is demonstrated by a case study.