Abstract

Abstract
Dynamic logic with binders D? has been introduced as an institution for the development of reactive systems based on model class semantics. The satisfaction relation of this logic was, however, not abstract enough to enjoy the modal invariance property (bisimilar models should satisfy the same sentences). We recently overcame this problem by proposing an observational satisfaction relation where the equality on states is interpreted by bisimilarity of states. This entailed, however, a price to pay - the satisfaction condition required for institutions was lost. This paper works on this limitation by establishing a behavioural semantics for D? parametric to behavioural structures - families of equivalence relations on the states of each model. Such structures are taken in consideration in the signature category and, in particular, for the definition of signature morphisms. We show that with these changes we get again an institution with a behavioural model class semantics. The framework is instantiated with specific behavioural structures, resulting in the novel Institution of Crucial Actions. © 2017, Springer International Publishing AG.

Abstract

Abstract
Robotic technologies are continuously transforming the domestic and the industrial environments. Recently the Robotic Operating System (ROS), has been widely adopted both by industry and academia, becoming one of the most popular middleware frameworks for developing robot applications. Guaranteeing the correct behaviour of robotic systems is, however, challenging due to their potential for parameterization and heterogeneity. Although different approaches exist, focusing on concrete domain spaces for specific scenarios, no general approach to reason about ROS systems has yet arisen. This paper proposes an approach to model and verify ROS systems using real time properties, focusing on one of the main features of ROS, the communication between nodes. It takes low-level parameters into account, such as queue sizes and timeouts, and uses timed automata as the modelling language. The robot Kobuki is used as a complex case study, over which properties are automatically verified using the UPPAAL model checker, enabling the identification of problematic parameter combinations.

Abstract

Abstract
Applications based on micro or web services have had significant growth due to the exponential increase in the use of mobile devices. However, using such kind of loosely coupled interfaces provides almost no guarantees to the developer in terms of evolution. Changes to service interfaces can be introduced at any moment, which may cause the system to fail due to mismatches between communicating parts. In this paper, we present a programming model that allows the development of web service applications, server end-points and their clients, in such a way that the evolution of services' implementation does not cause the disruption of the client. Our approach is based on a type based code slicing technique that ensures that each version only refers to type compatible code, of the same version or of a compatible version, and that each client request is redirected to the most recent type compatible version implemented by the server. We abstract the notion of version and parametrize type compatibility on the relation between versions. The relation between versions is tagged with compatibility levels, so to capture the common conventions used in software development. Our implementation allows multiple versions of a service to be deployed simultaneously, while reusing code between versions in a type safe way. We describe a prototype framework, based on code transformation, for server-side JavaScript code, and using Flow as verification tool. © 2017 IEEE.