No description available.

Running critical applications, such as e-commerce, in a distributed environment requires assurance of the identities of the participants communicating with each other. Providing such assurance in a distributed environment is a difficult task. The goal of a security protocol is to overcome the vulnerabilities of a distributed environment by providing a secure way to disseminate critical information into the network. However, designing a security protocol is itself an error-prone process. In addition to employing an authentication protocol, one also needs to make sure that the protocol successfully achieves its authentication goals. The Distributed Temporal Protocol Logic (DTPL) provides a language for formalizing both local and global properties of distributed communicating processes. The DTPL can be effectively applied to security protocol analysis as a model checker. Although, a model checker can determine flaws in a security protocol, it can not provide proof of the security properties of a protocol. In this research, we extend the DTPL language and construct a set of axioms by transforming the unified framework of SVO logic into DTPL. This results into a deductive style proof-based framework for the verification of authentication protocols. The proposed framework represents authentication protocols and concisely proves their security properties. We formalize various features essential for achieving authentication, such as message freshness, key association, and source association in our framework. Since analyzing security protocols greatly depends upon associating a received message to its source, we separately analyze the source association axioms, translate them into our framework, and extend the idea for public-key protocols. Developing a proof-based framework in temporal logic gives us another verification tool in addition to the existing model checker. A security property of a protocol can either be verified using our approach, or a design flaw can be identified using the model checker. In this way, we can analyze a security protocol from both perspectives while benefiting from the representation of distributed temporal protocol logic. A challenge-response strategy provides a higher level of abstraction for authentication protocols. Here, we also develop a set of formulae using the challenge-response strategy to analyze a protocol at an abstract level. This abstraction has been adapted from the authentication tests of the graph-theoretic approach of strand space method. First, we represent a protocol in logic and then use the challenge-response strategy to develop authentication tests. These tests help us find the possibility of attacks on authentication protocols by investigating the originator of its received messages. Identifying the unintended originator of a received message indicates the existence of possible flaws in a protocol. We have applied our strategy on several well-known protocols and have successfully identified the attacks.

Embedded systems are becoming increasingly common in our everyday lives. As techonology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must still fulfill strict requirements on reliability and correctness. This thesis proposes a formal verification methodology which smoothly integrates with component-based system-level design using a divide and conquer approach. The methodology assumes that the system consists of several reusable components. Each of these components are already formally verified by their designers and are considered correct given that the environment satisfies certain properties imposed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques. The verification methodology as well as the underlying theoretical framework and algorithms are presented in the thesis. Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply it on real-life examples. / <p>Report code: LiU-Tek-Lic-2003:57.</p>

Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs) are reusable PLC components that can be composed to implement the required system behaviour. A higher quality system may be realized if the FBs are pre-certified to be compliant with an international standard such as IEC 61131-3. Unfortunately, the set of programming notations defined in IEC 61131-3 lack well-defined formal semantics. As a result, tool vendors and users of PLCs may have inconsistent interpretations of the expected system behaviour. To address this issue, we propose an engineering method for formally verifying the conformance of candidate implementations of FBs (and their compositions) to their high-level, input-output requirements. The proposed method is sufficiently general to handle FBs supplied by IEC 61131-3, and industrial FB applications involving real-time requirements. Our method involves several steps. First, we use tabular expressions to ensure the completeness and disjointness of the requirements for the FB. Second, we formalize the candidate implementation(s) of the FB in question. Third, we state and prove theorems regarding the consistency and correctness of the FB. All three steps are performed using the Prototype Verification Systems (PVS) proof assistant. As a first case study, we apply our approach to the IEC 61131-3 standard to examine the entire library of FBs and their supplied implementations described in structured text (ST) and function block diagrams (FBDs). As a second case study, we apply our approach to two realistic sub-systems taken from the nuclear domain. Applying the proposed method, we identified three kinds of issues: ambiguous behavioural descriptions, missing assumptions, and erroneous implementations. Furthermore, we suggest solutions to these issues. / Thesis / Doctor of Philosophy (PhD) / A formal verification approach for the function block based control systems

This work investigates possible improvements to an existing annotation inference tool. The tool is part of a toolchain that aims to automate the process of software verification using formal methods. The purpose of the annotations is to facilitate the use of deductive verification, which is the formal method used in this project for proving that a given program meets its specifications. In the project, two categories of annotations are established. The first category is the category of functional annotations. These annotations describe the behavior of a function or a module. The other category is what we call auxiliary annotations. These annotations describe properties that are necessary for proving the correctness of the functional annotations. The tool that this work tries to improve is dedicated to inferring the auxiliary annotations. To our knowledge, this is the first tool of its kind to automatically infer auxiliary annotations for a complete module given the module’s source code and its interface specifications. The work contributed in four areas: inferring annotations from the interface specifications of a module and propagating these annotations to all the helper functions used in the module; inferring annotations for floating-point constructs; inferring annotations for pointer constructs; and finally, inferring annotations for array constructs. The improved tool was tested on production embedded code used in the heavy automotive industry. The results demonstrated a considerable improvement and were in line with earlier findings. The work confirms the feasibility and usability of auxiliary annotation inference in this scope. / Detta arbete undersöker möjliga förbättringar av ett befintligt verktyg för härledning av annoteringar (annotations). Verktyget är en komponent i en verktygskedja som syftar till att automatisera processen för mjukvaruverifiering med formella metoder. Syftet med annoteringarna är att underlätta användningen av deduktiv verifiering, vilket är den formella metod som används i detta projekt för att bevisa att ett givet program uppfyller dess specifikationer. I projektet fastställs två kategorier av annoteringar. Den första kategorin är kategorin funktionella annoteringar. Dessa annoteringar beskriver beteendet hos en funktion eller en modul. Den andra kategorin är vad vi kallar hjälp annoteringar (auxiliary annotations). Dessa annoteringar beskriver egenskaper som är nödvändiga för att bevisa korrektheten av de funktionella annoteringarna. Verktyget som detta arbete försöker förbättra är dedikerat till att härleda hjälp annoteringar. Arbetet bidrog inom fyra områden: att härleda annoteringar från gränssnittsspecifikationerna (interface specifications) för en modul och sprida dessa annoteringar till alla hjälpfunktioner som används i modulen; härleda annoteringar för flyttalskonstruktioner (floating-point constructs); härleda annoteringar för pekarkonstruktioner; och slutligen, härleda annoteringar för arraykonstruktioner. Det förbättrade verktyget testades på produktionsinbyggdad kod som används inom fordonsindustrin. Resultaten visade en avsevärd förbättring och var i linje med tidigare resultat. Arbetet bekräftar genomförbarheten och användbarheten av hjälpannoteringshärledning i projektets omfattning.

No description available.

The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library. / Thesis / Doctor of Philosophy (PhD) / The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library.

<p>Interval arithmetic is used to enclose roundoff, truncation, and modeling errors in interval methods, thus obtaining numerical methods with automatic verification of the results. The Fundamental Theorem of Interval Arithmetic (FTIA) shows that, when evaluating an expression using interval arithmetic, the computed result contains the mathematically correct value of the expression.</p> <p>Decorations were introduced in the IEEE P1788 working group for standardizing interval arithmetic. Their role is to help track properties of interval evaluations. That is, we wish to say if a function is defined, undefined, or continuous in its inputs. Moreover, decorations act as local exception flags and do not lead to interruption of the computations. The FTIA plus the decoration system is expanded into the Fundamental Theorem of Decorated Interval Arithmetic (FTDIA).</p> <p>Several versions of this theorem are formulated and proved by J. Pryce. This thesis formalizes and proves the core of this theorem (version 3.0 of the IEEE-P1788 proposal) using the theorem prover Coq. Namely, we prove it for the common case where all the inputs to a function are non-empty intervals.</p> <p>There are two distinctive features of our formalization and proof. First, we define the semantics of an interval as a set of real numbers (including the empty set), and we do not impose any other restrictions on such a set, except that models of this interval can decide if the set is empty or not. For example, an interval need not be closed and bounded, as in traditional interval arithmetic. Second, our formalization and proof do not rely on specific interval operations: it works with any interval operation that satisfies the requirements for decorated interval library operations.</p> <p>As the FTDIA is central to the IEEE-P1788 proposal, the correctness of the FTDIA is crucial. Our mechanized proof can give the research community in interval computations much confidence in its correctness. The current version of the FTDIA (in P1788 version 8.0) is slightly different from the theorem proved here. Modifying our proof to reflect this is left as future work.</p> / Doctor of Philosophy (PhD)

Yes / P colonies, tissue-like P systems with very simple components, have received constant attention from the membrane computing community and in the last years several new variants of the model have been considered. Another P system model, namely kernel P system, integrating the most successfully used features of membrane systems, has recently attracted interest and some important developments have been reported. In this paper we study connections among several classes of P colonies and kernel P systems, by showing how the behaviour of these P colony systems can be represented as kernel P systems. An example illustrates the way it is modelled by using P colonies and kernel P systems and some properties of it are formally proved in the latter approach. / Grant No. K 120558 of the NKFIH—National Research, Development, and Innovation Office, Hungary; Romanian National Authority for Scientific Research, CNCS-UEFISCDI (Project No. PN-III-P4-ID-PCE-2016-0210).

Yes / Structural and behavioural properties of models are very important in development of complex systems and applications. In this paper, we investigate such properties for some classes of SN P systems. First, a class of SN P systems associated to a set of routing problems are investigated through their matrix representation. This allows to make certain connections amongst some of these problems. Secondly, the behavioural properties of these SN P systems are formally verified through a natural and direct mapping of these models into kP systems which are equipped with adequate formal verification methods and tools. Some examples are used to prove the effectiveness of the verification approach. / EPSRC research grant EP/R043787/1; DOST-ERDT research grants; Semirara Mining Corp; UPD-OVCRD;