Advanced Formal Methods for Reactive Systems Engineering

Abstract : Significant scientific progress was made during the final year of this grant. The primary accomplishment was improving the performance of the Probabilistic I/O Automata (PIOA) Tool and comparing its performance to the PRISM model checker. The authors also designed and implemented the Aristotle runtime verification tool suite and applied it to the Linux kernel, as well as the GMC software model checker for GCC. They also developed and implemented a generic, on-the-fly technique for checking the correctness of real-time systems. This report contains a list of 13 papers submitted or published under ARO sponsorship; the names of scientific personnel supported by the project; a summary of scientific progress and accomplishments with regard to process-algebraic language for PIOA, Monte Carlo model checking, efficient modeling of excitable biological cells using hybrid automata, and safety/liveness semantics for UML 2.0 sequence diagrams; architectural system modeling; and technology transfer.