In our setting, verification is a process that checks whether a device's program (implementation) has been produced according to its corresponding requirements specification. Ideally a client builds the requirements specification of a program and asks a developer to produce the actual program according to the requirements specification it provides. After the program is built, a verifier is asked to verify the program. However, nowadays verification methods usually require good knowledge of the program to be verified and thus sensitive information about the program itself can be easily leaked during the process. In this thesis, we come up with the notion of secure and trusted verification which allows the developer to hide non-disclosed information about the program from the verifier during the verification process and a third party to check the correctness of the verification result. Moreover, we formally study the mutual trust between the verifier and the developer and define the above notion in the context of both an honest and a malicious developer. Besides, we implement the notion above both in the setting of an honest and a malicious developer using cryptographic primitives and tabular expressions. Our construction allows the developer to hide the modules of a program and the verifier to do some-what white box verification. The security properties of the implementation are also formally discussed and strong security results are proved to be achieved. / Thesis / Master of Science (MSc)

Model-based development (MBD) is an increasingly used approach for the development of embedded control software, with Matlab Simulink/Stateflow as the widely accepted language. The adoption of this development paradigm is prevalent in many safety-critical domains, including the automotive industry. With an increasing reliance on software for controlling vehicle functionality and the yearly advent of new vehicle features, automotive models have been growing in size and complexity, causing them to become increasingly difficult to maintain, refactor, and test. Given the centrality of models in MBD, it is a requisite that they be maintained under well-defined and principled software development processes that use precise notation to document system requirements and behavioural design description. Tabular methods have long been used for defining decision-making logic in software, due to their concise and precise manner of communicating complex behaviour, so it is not surprising that they are finding increased use in automotive software models. Thus their presence in Simulink models is increasingly prominent in the implementation of complex behaviour in production code. As a result of the safety-critical nature of the automotive industry, as well as the increasing size and complexity of its models, reliable refactoring and simplification techniques for tabular expressions are becoming an important need for automotive companies. To address this need, this thesis presents a methodology for refactoring complex tabular designs to improve requirements traceability with a focus on Matlab Simulink/Stateflow and the MBD approach. A case study of industrial examples from an automotive partner are used to motivate the work and demonstrate the proposed methodology's effectiveness in reducing design size and complexity, while also increasing testability and requirements traceability. / Thesis / Master of Applied Science (MASc)

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