Accession Number:

ADA433610

Title:

Advanced Formal Methods for Reactive Systems Engineering

Descriptive Note:

Final progress rept. 1 Feb 2004-31 Jan 2005

Corporate Author:

STATE UNIV OF NEW YORK AT STONY BROOK DEPT OF COMPUTER SCIENCE

Report Date:

2005-05-04

Pagination or Media Count:

5.0

Abstract:

Significant scientific progress was made during the final year of this grant. The primary accomplishment was improving the performance of the Probabilistic IO 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 safetyliveness semantics for UML 2.0 sequence diagrams architectural system modeling and technology transfer.

Subject Categories:

  • Operations Research
  • Computer Programming and Software
  • Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE