The talk introduces two corecursion schemes for streamgenerating functions, scans and convolutions, and discusses their properties. As an application of the framework, a calculational proof of Moessners intriguing theorem is presented.
read moreModel checking GOAL agents
As the theoretical foundations of agent-oriented programming became better understood by the end of the 1990s, researchers became interested in model checking agent programs. Model checking, introduced by the late 1970s, is a technique for establishing automatically whether a system satisfies a given specification. Although progress has been made over …
read moreJOLIE: a service oriented language
Service oriented computing is an emerging paradigm for programming distributed applications based on services. Services are simple software elements that supply their functionalities by exhibiting their interfaces and that can be invoked by exploiting simple communication primitives. The emerging mechanism exploited in service oriented computing for composing services âin …
read moreDecidability properties for fragments of CHR
We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity gt;0$). Both languages allow the use of the $=$ built-in in the body of rules, thus are built on …
read moreCoalgebraic Representation Theory of Fractals
We develop a representation theory in which a point of a fractal specified by metric means (by a variant of an iterated function system, IFS) is represented by a suitable equivalence class of infinite streams of symbols. The framework is categorical: symbolic representatives carry a final coalgebra; an IFS-like metric …
read moreFormalising Domain-Specific Modelling Languages
We propose an approach for formalising Domain-Specific Modelling Languages (DSML). Our approach is based on representing models and metamodels as specifications in the Maude algebraic specification language. This provides us with abstract definitions of essential concepts of DSML (model-to-metamodel conformance, operational semantics, and model transformations) that naturally capture their intutive …
read moreAlgebraic and Coalgebraic Reasoning in Agent-Based Models -- A Case Study From Ecology
Agent-based models (ABMs) are a new and increasingly popular class of simulation software in natural and social sciences. They combine state-based and behaviour-based modelling paradigms for empirical phenomena in an unorthodox way that currently has no sound theoretical foundation. As we have demonstrated in previous work, the state/behaviour dichotomy …
read moreMessage sequence monitoring without code instrumentation
One of the problems in software testing is to specify and verify the execution of a sequence of method calls in object-oriented software. In this paper, we introduce JMSeq to propose a formal method based on context-free grammars to specify a sequence of method calls; it provides a simple way …
read more(Abstraction and Refinement of) Timed Constraint Automata in the ECT
In this talk, I will give a tool demonstration of how Timed Constraint Automata (TCA) have been integrated into the ECT. In particular, I will present the TCA editor, the translation into propositional formulas plus linear arithmetic, and the abstraction-refinement backend used for model checking.
read moreModel checking a language with unbounded object creation
We introduce a block-structured programming language which supports object creation, global variables, static scope and recursive procedures with local variables. Because of the combination of recursion, local variables and object creation, the behavior of the program is determined by infinitely many different states. However, we show that a program can …
read more