Assessing and assuring interoperability of a genomics file format

Background: Bioinformatics software tools operate largely through the use of specialized genomics file formats. Often these formats lack formal specification, and only rarely do the creators of these tools robustly test them for correct handling of input and output. This causes problems in interoperability between different tools that, at best, wastes time and frustrates users. At worst, interoperability issues could lead to undetected errors in scientific results. Methods: We sought (1) to assess the interoperability of a wide range of bioinformatics software using a shared genomics file format and (2) to provide a simple, reproducible method for enhancing interoperability. As a focus, we selected the popular BED file format for genomic interval data. Based on the file format's original documentation, we created a formal specification. We developed a new verification system, Acidbio (https://github.com/hoffmangroup/acidbio), which tests for correct behavior in bioinformatics software packages. We crafted tests to unify correct behavior when tools encounter various edge cases—potentially unexpected inputs that exemplify the limits of the format. To analyze the performance of existing software, we tested the input validation of 80 Bioconda packages that parsed the BED format. We also used a fuzzing approach to automatically perform additional testing. Results: Of 80 software packages examined, 75 achieved less than 70% correctness on our test suite. We categorized multiple root causes for the poor performance of different types of software. Fuzzing detected other errors that the manually designed test suite could not. We also created a badge system that developers can use to indicate more precisely which BED variants their software accepts and to advertise the software's performance on the test suite. Discussion: Acidbio makes it easy to assess interoperability of software using the BED format, and therefore to identify areas for improvement in individual software packages. Applying our approach to other file formats would increase the reliability of bioinformatics software and data.

A Comprehensive Formalization of AADL with Behavior Annex

In safety-critical fields, architectural languages such as AADL (Architecture Analysis and Design Language) have been playing an important role, and the analysis of the languages and systems designed by them is a challenging research topic. At present, a formal method has become one of the main practices in software engineering for strict analysis, and it has been applied on the tools of formalization and analysis. The formal method can be used to find and resolve the problems early by describing the system with precise semantics and validating the system model. This article studies the comprehensive formal specification and verification of AADL with Behavior annex by the formal method. The presentation of this specification and semantics is the aim of this article, and the work is illustrated with an ARINC653 model case study in Isabelle/HOL.

Description of the Imperative Programming Language in Haskell

When creating a programming language, it is necessary to determine its syntax and semantics. The main task of syntax is to describe all constructions that are elements of the language. For this purpose, a specific syntax highlights syntactically correct sequences of characters of the language alphabet. Most often it is a finite set of rules that generate an infinite set of all construction languages, such as the extended Backus-Naur (BNF) form.To describe the semantics of the language, the preference is given to the abstract syntax, which in real programming languages is shorter and more obvious than specific. The relationship between abstract syntax objects and the syntax of the program in compilers solves the parsing phase.Denotational semantics is used to describe semantics. Initially, it records the denotations of the simplest syntactic objects. Then, with each compound syntactic construction, a semantic function is associated, which by denotations of components of a design calculates its value – denotation. Since the program is a specific syntactic construction, its denotation is possible to determine using the appropriate semantic function. Note that the program itself is not executed when calculating its denotation.The denotative description of a programming language includes the abstract syntax of its constructions, denotations – the meanings of constructions and semantic functions that reflect elements of abstract syntax (language constructions) in their denotations (meanings).The use of the functional programming language Haskell as a metalanguage is considered. The Haskell type system is a good tool for constructing abstract syntax. The various possibilities for describing pure functions, which are often the denotations of programming language constructs, are the basis for the effective use of Haskell to describe denotational semantics.The paper provides a formal specification of a simple imperative programming language with integer data, block structure, and the traditional set of operators: assignment, input, output, loop and conditional. The ability of Haskell to effectively implement parsing, which solves the problem of linking a particular syntax with the abstract, allows to expand the formal specification of the language to its implementation: a pure function — the interpreter.The work contains all the functions and data types that make up the interpreter of a simple imperative programming language.

A Verified Formal Specification of A Secured Communication Method For Smart Card Applications

In remote villages without access to modern IT technology, simple devices such as smartcards can be used to carry out business transactions. These devices typically store multiple business applications from multiple vendors. Although devices must prevent malicious or accidental security breaches among the applications, a secure communication channel between two applications from different vendors is often required. In this paper, first, we propose a method of establishing secure communication channels between applications in embedded operating systems that run on multi-applet smart cards. Second, we enforce the high assurance using an intransitive noninterference security policy. Thirdly, we formalize the method through the Z language and create the formal specification of the proposed secure system. Finally, we verify its correctness using Rushby's unwinding theorem.

PRASH: A Framework for Privacy Risk Analysis of Smart Homes

Smart homes promise to improve the quality of life of residents. However, they collect vasts amounts of personal and sensitive data, making privacy protection critically important. We propose a framework, called PRASH, for modeling and analyzing the privacy risks of smart homes. It is composed of three modules: a system model, a threat model, and a set of privacy metrics, which together are used for calculating the privacy risk exposure of a smart home system. By representing a smart home through a formal specification, PRASH allows for early identification of threats, better planning for risk management scenarios, and mitigation of potential impacts caused by attacks before they compromise the lives of residents. To demonstrate the capabilities of PRASH, an executable version of the smart home system configuration was generated using the proposed formal specification, which was then analyzed to find potential attack paths while also mitigating the impacts of those attacks. Thereby, we add important contributions to the body of knowledge on the mitigations of threat agents violating the privacy of users in their homes. Overall, the use of PRASH will help residents to preserve their right to privacy in the face of the emerging challenges affecting smart homes.

Vacuity in synthesis

In reactive synthesis, one begins with a temporal specification $$\varphi $$ φ , and automatically synthesizes a system $$M$$ M such that $$M\models \varphi $$ M ⊧ φ . As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies $$\varphi $$ φ non-vacuously, then M is likely to be closer to the user’s intent, because it satisfies $$\varphi $$ φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.