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.

Abstract This article describes a framework to formally model and analyse human behaviour. This is shown by a simple case study of a chocolate vending machine, which represents many aspects of human behaviour. The case study is modelled and analysed using the Maude rewrite system. This work extends a previous work by Basuki which attempts to model interactions between human and machine and analyse the possibility of errors occurring in the interactions. By redesigning the interface, it can be shown that certain kinds of error can be avoided for some users. This article overcomes the limitation of Basuki’s approach by incorporating many aspects of user behaviour into a single user model, and introduces a more natural approach to model human–computer interaction.