HILT 2013             ACM logo - Advancing Computing as a Science & Profession

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Invited Presentation:
Up and Out: Scaling Formal Analysis Using Model-Based Development and Architecture Modeling

Wednesday, November 13, 2:00-3:30pm

Michael Whalen

Abstract

Systems are naturally constructed in hierarchies in which design choices made at higher levels of abstraction levy requirements on system components at lower levels of abstraction. Thus, whether an aspect of the system is a design choice or a requirement depends largely on one’s vantage point within the hierarchy of system components. Furthermore, systems are often constructed middle-out rather than top-down; compatibility with existing systems and architectures, or availability of specific components influences high-level requirements. We believe that requirements and architectural design should be more closely aligned: that requirements models must account for hierarchical system construction, and that architectural design notations must better support specification of requirements for system components.

In this presentation, I describe tools supporting iterative development of architecture and verification based on software models. We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe requirements at different levels of abstraction for compositional verification. To describe and verify component-level behavior, we use Simulink and Stateflow and multiple analysis tools.


Created on 29 May 2014;  website comments and corrections to ClydeRoby at ACM.Org