Accession Number:

AD1032016

Title:

REQUIREMENTS PATTERNS FOR FORMAL CONTRACTS IN ARCHITECTURAL ANALYSIS AND DESIGN LANGUAGE (AADL) MODELS

Descriptive Note:

Technical Report,01 Oct 2015,01 Oct 2016

Corporate Author:

Rockwell Collins Bloomington United States

Personal Author(s):

Report Date:

2017-04-17

Pagination or Media Count:

42.0

Abstract:

English language requirements are often used to specify the behavior of complex cyber-physical systems. The process of transforming these requirements to a formal specification language is often challenging, especially if the specification language does not contain constructs analogous to those used in the original requirements. For example, requirements often contain real-time constraints, but many specification languages for model checkers have discrete time semantics. Work in specification patterns helps to bridge these gaps, allowing straightforward expression of common requirements patterns in formal languages. In this report we demonstrate how we support real-time specification patterns in the Assume Guarantee Reasoning Environment AGREE using observers. We demonstrate that there are subtle challenges, not mentioned in previous literature, to express real-time patterns accurately using observers. We demonstrate that these patterns are sufficient to model real-time requirements for a real-world avionics systems.

Subject Categories:

  • Linguistics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE