Search

To react to unforeseen circumstances or amend abnormal situations in communication-centric systems, programmers are in charge of “undoing” the interactions which led to an undesired state. To assist this task, session-based languages can be endowed with reversibility mechanisms. In this paper we propose a language enriched with programming facilities to commit session interactions, to roll back the computation to a previous commit point, and to abort the session. Rollbacks in our language always bring the system to previous visited states and a rollback cannot bring the system back to a point prior to the last commit. Programmers are relieved from the burden of ensuring that a rollback never restores a checkpoint imposed by a session participant different from the rollback requester. Such undesired situations are prevented at design-time (statically) by relying on a decidable compliance check at the type level, implemented in MAUDE. We show that the language satisfies error-freedom and progress of a session.

Space is important in the QUANTICOL project because the project case studies include smart transport, and quantitative modelling of transport has inherent spatial aspects. This deliverable presents a review of the literature about spatial modelling within and beyond computer science, and a classification of the different approaches reviewed. The objective of the classification is to make clear what approaches are available and how they differ from each other. This will be used to guide future work on spatial approaches within the project. Furthermore, the classification enables the identification of the approaches that have been used in the initial work on case studies in the realm of smart transport. This deliverable rst identifies the aspects of non-spatial modelling that are important in the context of the QUANTICOL project. Time can be modelled in a discrete or continuous manner. States can be discrete, representing attributes of an individual. For example, when considering bike sharing, inUse (busy), onStand (idle) or atWorkshop (under repair) might be appropriate states for a bike. Alternatively, states can be continuous representing an attribute (for example, seat height). In the case of discrete states, it is possible to perform aggregation by considering populations, namely how many individuals are in each state, and to acquire an understanding of the overall behaviour of the population, rather than of individuals. Mean-field techniques can be employed to transform a discrete population approach to one that considers continuous populations that approximate the discrete approach. To this context, space is introduced. Space can be discrete and described by a graph of locations. Depending on the structure of the graph and the parameters associated with locations and movement between locations, discrete space can be classified as regular or homogeneous. Space can be seen as continuous: as Euclidean space in one, two or three dimensions. Space can also be considered abstractly as topological space, whether discrete or continuous and this approach allows for reasoning about concepts such as adjacency and neighbourhoods. This deliverable describes the modelling techniques that are currently available for the different combinations of time, state, aggregation and space, giving both a tabular classification as well as high-level and formal descriptions of the techniques. For each representation, examples are given of its use in different disciplines, including ecology, biology, epidemiology and computer science. In particular, the modelling goals are considered for these techniques, and compared with the goals of the QUANTICOL project. This deliverable also has the aim of identifying disparate uses of terminology in various approaches. Both current and future case studies relevant to the project are classified in terms of how they use time, state, aggregation and space and nally conclusions are presented taking into account the literature reviewed, what has been modelled and what the goals of the project are for modelling of smart transport. The preliminary guidelines arising from the review and classification are to focus on patch models and associated techniques although continuous space models of individuals may be important in certain cases. Items proposed for further research are understanding and developing mean-field techniques, spatial and non-spatial moment closure methods and hybrid spatial approaches. The document closes with a future work plan for Work Package 2.