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

Ion channels and pumps play critical roles during sea urchin development including mediating the blocks to polyspermy, regulating left-right and dorsal-ventral axis specification, directing ventral PMC migration, and controlling biomineralization of the larval skeleton. We performed a screen of pharmacological ion channel inhibitors, and we chose two inhibitors to investigate further. First, we found that tricaine, a potent inhibitor of voltage-gated sodium channels (VGSCs), induces aberrant skeletal patterning in Lytechinus variegatus larvae. The larval skeleton is secreted by the primary mesenchyme cells (PMCs), which migrate within the blastocoel into a stereotypical pattern. We show that VGSC activity is required for normal PMC migration and skeletal patterning. Timed inhibitor studies identified VGSC activity as specifically required from early gastrula to the onset of late gastrula for normal skeletal patterning. Tricaine inhibits the voltage-gated sodium channel LvScn5a which is strongly expressed in the developing nervous system in pluteus larvae. We found that exogenous expression of an anesthetic-insensitive version of LvScn5a is sufficient to rescue hallmark tricaine-mediated skeletal patterning defects, demonstrating the specificity of the inhibitor. LvScn5a exhibits a ventrolateral ectodermal expression domain in gastrulating embryos that is spatiotemporally congruent with triradiate formation in the ventrolateral PMC clusters at the onset of skeletogenesis. This ectodermal territory normally expresses the patterning cue Wnt5, and we find that the expression of Wnt5 is dramatically spatially expanded by tricaine treatment. We also observe ectopic PMC clusters in tricaine-treated embryos. We found that knockdown of Wnt5 expression is sufficient to rescue tricaine-mediated skeletal patterning defects. These results are consistent with a model in which LvScn5a activity in the ventrolateral ectoderm functions to spatially restrict the expression of the ectodermal patterning cue Wnt5 that in turn induces PMC cluster formation. Together, these findings show that spatially restricted sodium channel activity regulates ectodermal cue expression that, in turn, regulates PMC differentiation and skeletal morphogenesis. Second, we show that V-type H⁺ ATPase (VHA) activity is required for specification of the dorsal-ventral (DV) axis. DV specification is controlled by the TGF-β signal Nodal that specifies the ventral territory and indirectly activates dorsal specification via induction of BMP 2/4 expression. Nodal expression occurs downstream of p38 MAPK, which is transiently, asymmetrically inactive on the presumptive dorsal side of the blastula embryo. VHA activity is required for that transient inactivation of p38 MAPK, and it is required for the subsequent spatial restriction of Nodal expression. We show that VHA inhibition is sufficient to induce global Nodal expression during the blastula stage, resulting in ventralization of the embryo. We show that this phenotype can be rescued by experimentally imposing asymmetric Nodal expression at the 4-cell stage. We discover a VHA-dependent voltage gradient across the DV axis and find that VHA activity is required for hypoxia inducible factor (HIF) activation. We show that neither hyperpolarization nor HIF activation is sufficient to perturb DV specification, which implicates a third unknown pathway connecting VHA activity and p38 MAPK symmetry breaking. These results are consistent with a model in which dorsal VHA activity is required to inhibit Nodal expression and signaling, potentially via dorsal p38 MAPK inhibition. Together, these studies demonstrate that ion channels are required for both DV specification and for normal skeletal patterning.

No description available.

No description available.

No description available.

No description available.

No description available.

No description available.

<p> It has been argued for some time that tabular representations of formal specifications can help in writing them, in understanding them, and in checking them. Recently it has been suggested that tabular representations also help in breaking down large verification and refinement conditions into a number of smaller ones.</p> <p> The article [32] developed the theory, but the real proof in terms of an implementation is not provided. This project is about formalizing tables in a theorem prover, Simplify, defining theorems of [32] in terms of functions written in the OCaml programming language, and conducting some case studies in verifying and refining realistic problems.</p> <p> A parser is designed to ease our job of inputting expressions. Pretty-print is also provided: all predicates and tables of the examples in our thesis are automatically generated.</p> <p> Our first example is a control system, a luxury sedan car seat. This example gives us an overall impression on how to prove correctness from tabular specification. The second example specifies a visitor information system. The design features of this example involve modeling properties and operations on sets, relations and functions by building self-defined axioms. The third example illustrates another control system, an elevator. Theorems of algorithmic refinements, stepwise data refinements, and the combination of algorithmic abstraction and data abstraction are applied correspondingly to different operations.</p> / Thesis / Master of Science (MSc)

Assurance Cases have been effectively used for improving the safety of real-time safety systems. However, until now, Assurance Case techniques have not been applied to building confidence in the correctness of Scientific Computing (SC) software. Our approach is to employ Assurance Case techniques to the case of a specific medical image analysis software, 3dfim+, and then generalize the results/template for other medical and SC software. Using the Goal Structuring Notation (GSN), we develop an Assurance Case to support the top goal that "Program 3dfim+ delivers correct outputs when used for its intended use/purpose in its intended environment." This claim is supported by several sub-claims, including the claims that high-quality requirements exist and that the implementation complies with the requirements. The full argument decomposes each sub-claim further until at the bottom level evidence is provided. The evidence provided includes the requirements documentation, test cases and expert review. To simplify the Assurance Case diagram, a new generic module, parameterized over quality, was developed to argue that each quality has been achieved. Evaluation of the full Assurance Case shows that this approach is feasible for building confidence in SC software, even in the practical situation where confidence is sought, but redesign and reimplementation are not possible. The exercise uncovered issues with the original documentation for 3dfim+, including missing assumptions, and ambiguity with the chosen sign convention. Furthermore, although no errors in output were found, the Assurance Case highlights that confidence in the original 3dfim+ software could be improved through additional checks for input validity. / Thesis / Master of Science (MSc)