Architecture-Based Verification

Spring 2009

James Choi
Bruce Krogh
Project description

This project concerns an architecture-based approach and tool to support the principled design and evaluation of alternative architectures for cyber-physical system (CPS) applications. Architecture description languages (ADLs) support the description of annotated structural representations that facilitate the evaluation of design tradeoffs in terms of important quality features such as performance, reliability, security, and maintainability. The proposed approach builds on existing software architecture tools that have worked well for complex software systems by developing a new CPS style with certain basic component and connector types to model physical systems, their interconnections, and the interaction between physical and cyber components. Specific work during the spring 2009 semester involves the implementation of two analysis tools implemented as ACME plug-ins for analyzing and verifying properties of CPS designs using Labelled Transition System Analyser (LTSA) for verifying finite-state processes (FSP) and PHAVer for verifying linear hybrid automata. These plug-ins will support the formal analysis of annotated architectural descriptions of cyber-physical systems.

Return to project list