Rascal (http://www.rascal-mpl.org) is a domain specific language (DSL) for meta programming. While originally focused on transformation and analysis of source code, initial experiments are currently performed to process other kinds of models. I will give some example of how (traditionally object-oriented) meta models are represented in Rascal …
read moreStrategic Executions of Choreographed Timed Normative Multi-Agent Systems
In this talk we describe a combined mechanism (and its implementation by means of rewrite strategies) for coordinating agents in timed multi-agent systems. What we combine is the timed extensions of two orthogonal coordination mechanisms wrt the dichotomy action/state. On the one hand, we have action-based artifacts, i.e …
read moreSpecifying Interfaces in Java in terms of Communication Histories using Attribute Grammars - part 1
We propose a new formal modeling language for the specification of interfaces in Java in terms of communication histories, i.e., sequences of messages. We show how attribute grammars provide a powerful separation of concerns between high-level protocol-oriented properties, which focus on the kind of messages sent and received, and …
read moreCreol goes Linda
We introduce Creol, a modeling language for concurrent distributed systems based on asynchronous communication. To illustrate Creol's concurrency and communication model we compare it to Java. We give a notion of deadlock for Creol programms and show how to model Creol programs in Linda (to provide deadlock detection in the …
read moreDelta Modeling
A software product line (SPL) is a family of software systems with well defined commonalities and variabilities. These systems (products) are uniquely identified by a set of features. But a feature is merely a label. To attach semantics to features, the code base for an SPL should be organized in …
read moreStochastic Activity Networks
Stochastic activity networks (SANs) are a stochastic generalization of Petri nets that have been defined for the modeling and analysis of distributed real-time systems. SANs were introduced in 1984 for the performance and dependability (performability) modeling of such systems. SAN models are more powerful and flexible than most other stochastic …
read moreCompositional and Computable Semantics for Modelling Hybrid Systems
Hybrid systems are dynamic systems combining discrete and continuous behaviour. It is important to have powerful modelling frameworks which support modular design via composition of subsystems, and automated software tools for simulation and verification. Unfortunately, it is a nontrivial task to provide a behavioural semantics for a modelling framework which …
read moreVerification of Software Product Lines
A software product line is a set of systems with well-defined commonalities and variabilities that are developed by managed reuse. Because of the huge number of possible configurations, it is crucial to guarantee critical system requirements. However, it is infeasible to formally verify each system in isolation. Instead, verification artifacts …
read moreSpecifying Behavior of Reo in mCRL2
In this ACG meeting, we present our approach to medeling and verification of Reo circuits using process specification language mCRL2 and the corresponding model checking toolset. We start from the encoding of Reo in mCRL2 according to its constraint automata semantics, and then discuss several lines of ongoing work on …
read moreLogic of Information Flow on Communication Channels
We present a logic to describe communcation channels and secret messages. Additionally, our logic can reason about communication protocols. We combine a Dynamic Epistemic Logic (DEL) perspective with ideas from Interpreted Systems (IS). Our framework models the communication channels underlying the information flow as well as the information flow itself …
read more