Search

This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied pi-calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so.

SDF3 is a syntax definition formalism that extends plain context-free grammars with features such as constructor declarations, declarative disambiguation rules, character-level grammars, permissive syntax, layout constraints, formatting templates, placeholder syntax, and modular composition. These features support the multi-purpose interpretation of syntax definitions, including derivation of type schemas for abstract syntax tree representations, scannerless generalized parsing of the full class of context-free grammars, error recovery, layout-sensitive parsing, parenthesization and formatting, and syntactic completion. This paper gives a high level overview of SDF3 by means of examples and provides a guide to the literature for further details.

Context-awareness refers to the ability to sense and adapt to context. With the rise of context-aware systems, designers are struggling with what variables should be sensed from the context. According to the definitions found in the literature, whether something belongs to context, has to do with whether it is relevant. However, what it means to be relevant is left implicit in these definitions. Most work on context-aware systems is based on assumptions of the context that should be taken into account. Hence, it is unclear how to decide whether something belongs to context or should be left out. In this paper, first we analyse what is meant with context and provide a definition. In this definition we introduce the notion of a context variable, defined as an attribute of an object that is relevant. Context is then defined as the set of context variables. We establish explicit criteria for deciding whether an attribute of an object is a context variable based on the proposed definition and the designer’s goal. We also provide a straightforward method to help designers to determine whether the criterion is met and a variable should be included in the context. This method is based on filling out a scheme to describe context variables.

The recent active development of Internet of Things (IoT) solutions in various domains has led to an increased demand for security, safety, and reliability of these systems. Security and data privacy are currently the most frequently discussed topics; however, other reliability aspects also need to be focused on to maintain smooth and safe operation of IoT systems. Until now, there has been no systematic mapping study dedicated to the topic of interoperability and integration testing of IoT systems specifically; therefore, we present such an overview in this study. We analyze 803 papers from four major primary databases and perform detailed assessment and quality check to find 115 relevant papers. In addition, recently published testing techniques and approaches are analyzed and classified; the challenges and limitations in the field are also identified and discussed. Research trends related to publication time, active researchers, and publication media are presented in this study. The results suggest that studies mainly focus only on general testing methods, which can be applied to integration and interoperability testing of IoT systems; thus, there are research opportunities to develop additional testing methods focused specifically on IoT systems, so that they are more effective in the IoT context.

Given the considerable ongoing research interest in collaborative multidisciplinary modelling and co-simulation, it is worth considering the features of model-based techniques and tools that deliver benefits to cyber-physical systems developers. The European project “Integrated Tool Chain for Model-based Design of Cyber-Physical Systems” (INTO-CPS) has developed a well-founded tool chain for CPS design, based on the Functional Mock-up Interface standard, and supported by methodological guidance. The focus of the project has been on the delivery of a sound foundation, an open chain of compatible and usable tools, and a set of accessible guidelines that help users adapt the technology to their development needs.

This work examines the use of co-simulation in the development and optimisation of a steering system for a driverless industrial size lawn mower. Initial models of the kinematics, dynamics and steering control system are co-simulated to investigate the performance of the controller in a virtual setting. The co-simulation consists of a Continuous-Time (CT) model of the lawn mower kinematics and dynamics and a Discrete-Event (DE) model of the steering controller modelled in VDM-RT. The models are co-simulated by the use of the Co-simulation Orchestration Engine which is a core tool of the INTO-CPS project. The CT model of the lawn mower is calibrated and verified experimentally. The result of co-simulation is in a similar fashion verified by comparing the simulated and measured trajectories.

Writing correct C programs is well-known to be hard, not least due to the many interesting language features intrinsic to C. Writing secure C programs is even harder and, at times, seemingly impossible. To improve on this situation the US CERT has developed and published a set of coding standards, the ``CERT C Secure Coding Standard'', that enumerates a number of rules and recommendations with the aim of making C programs (more) secure. Automated tool support is essential for certifying that a given system is in compliance with the rules and/or recommendations of the standards. In this paper we report on work-in-progress with integrating two state of the art analysis tools, Clang and Coccinelle, into a combined tool perfectly suited for analysing and certifying C programs according to, e.g., the CERT C Secure Coding standard or the MISRA (the Motor Industry Software Reliability Assocation) C standard. We further argue that such a tool must be highly adaptable and customisable to individual software projects as well as to the certification rules required by a given standard. Clang is the C frontend for the LLVM compiler/virtual machine project which includes a comprehensive set of static analyses and code code checkers. Coccinelle is a program transformation tool and bug-finder developed originally for the Linux kernel but has been successfully used to find bugs in other Open Source projects such as WINE and OpenSSL.

The UML (Unified Modeling Language) state diagram notation by M. Fowler and K. Scott (2000) is a graphical language which comprises an extensive set of constructs with good structural semantics but lack of a formal behavioral semantics. With this regard, we have used the Hoare's CSP (Communicating and Sequential Processes) to formalize the behavior of UML SD. The fact that CSP is supported by model-checkers such as FDR enables a system design using a state diagram to be formally checked during design stage. This paper presents the formalization which would allow us to reason about the behavior of UML SD in CSP.

We propose a formal model of trust informed by the Global Computing scenario and focusing on the aspects of trust formation, evolution, and propagation. The model is based on a novel notion of trust structures which, building on concepts from trust management and domain theory, feature at the same time a trust and an information partial order.