Abstract
This tool paper presents the High-Assurance ROS (HAROS) framework. HAROS is a framework for the analysis and quality improvement of robotics software developed using the popular Robot Operating System (ROS). It builds on a static analysis foundation to automatically extract models from the source code. Such models are later used to enable other sorts of analyses, such as Model Checking, Runtime Verification, and Property-based Testing. It has been applied to multiple real-world examples, helping developers find and correct various issues.

Abstract
We extend hybrid dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations: The first one relies on observational abstraction from the ordinary model class of a specification Sp by considering its closure under weak bisimulation. The second one uses an observational satisfaction relation for the axioms of the specification Sp, which relaxes the interpretation of state variables and the satisfaction of modal formulae by abstracting from silent transitions. We establish a formal relationship between both approaches and show that they are equivalent under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions. As a particular outcome we provide an invariance theorem and show the Hennessy-Milner property for weakly bisimilar labelled transition systems and observational satisfaction. In the second part of the paper we integrate our results in a development methodology for reactive systems leading to two versions of observational refinement. We provide conditions under which both kinds of refinement are semantically equivalent, involving implementation constructors for relabelling, hiding, and parallel composition.

Abstract

Abstract
Dynamic Epistemic Logic (DEL) is used in the analysis of a wide class of application scenarios involving multi-agents systems with local perceptions of information and knowledge. In its classical form, the knowledge of epistemic states is represented by sets of propositions. However, the complexity of the current systems, requires other richer structures, than sets of propositions, to represent knowledge on their epistemic states. Algebras, graphs or distributions are examples of useful structures for this end. Based on this observation, we introduced a parametric method to build dynamic epistemic logics on-demand, taking as parameter the specific knowledge representation framework (e.g., propositional, equational or even a modal logic) that better fits the problems in hand. In order to use the built logics in practices, tools support is needed. Based on this, we extended our previous method with a parametric construction of complete proof calculi. The complexity of the model checking and satisfiability problems for the achieved logics are provided. © 2021, IFIP International Federation for Information Processing.

Abstract
We propose E-down arrow((D) over right arrow)-logic as a formal foundation for the specification and development of event-based systems with data states. The framework is presented as an institution in the sense of Goguen and Burstall and the logic itself is parametrised by an underlying institution (D) over right arrow whose structures are used to model data states. E-down arrow((D) over right arrow)-logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. It uses modal diamond and box operators over complex actions adopted from dynamic logic. Atomic actions are pairs e/psi where e is an event and psi a state transition predicate capturing the allowed reactions to the event. Towrite concrete specifications of recursive process structureswe integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that E-down arrow((D) over right arrow)-logic is powerful enough to characterise the semantics of an operational specification by a single E-down arrow((D) over right arrow)-sentence. Thus the whole (formal) development process for event/data-based systems relies on E-down arrow((D) over right arrow)-logic and its semantics as a common basis. It is supported by a variety of implementation constructors which can express, among others, event refinement and parallel composition. Due to the genericity of the approach, it is also possible to change a data state institution during system development when needed. All steps of our formal treatment are illustrated by a running example.

Abstract
The vast datasets produced in human genomics must be efficiently stored, transferred, and processed while prioritizing storage space and restore performance. Balancing these two properties becomes challenging when resorting to traditional data compression techniques. In fact, specialized algorithms for compressing sequencing data favor the former, while large genome repositories widely resort to generic compressors (e.g., GZIP) to benefit from the latter. Notably, human beings have approximately 99.9 percent of DNA sequence similarity, vouching for an excellent opportunity for deduplication and its assets: leveraging inter-file similarity and achieving higher read performance. However, identity-based deduplication fails to provide a satisfactory reduction in the storage requirements of genomes. In this article, we balance space savings and restore performance by proposing GenoDedup, the first method that integrates efficient similarity-based deduplication and specialized delta-encoding for genome sequencing data. Our solution currently achieves 67.8 percent of the reduction gains of SPRING (i.e., the best specialized tool in this metric) and restores data 1.62x faster than SeqDB (i.e., the fastest competitor). Additionally, GenoDedup restores data 9.96x faster than SPRING and compresses files 2.05x more than SeqDB.