Model-Checking of Component-Based Event-Driven Real-Time Embedded Software

Abstract

As complexity of real-time embedded software grows, it is desirable to use formal verification techniques to achieve a high level of assurance. We discuss application of model-checking to verify system-level concurrency properties of component-based real-time embedded software based on CORBA Event Service, using Avionics Mission Computing software as an application example. We use the process algebra FSP to formalize specification of software components and system architecture, previously only available in the form of natural language and prone to misinterpretation and misunderstanding, and use model-checking to verify system-level concurrency properties. We also discuss effective techniques for coping with the state-space explosion problem by exploiting application domain semantics. We have applied our analysis techniques to realistic application scenarios provided by our industry partner to demonstrate their utility and power.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2005
Accession Number
ADA465755

Entities

People

  • Kang G. Shin
  • Zonghua Gu

Organizations

  • University of Virginia

Tags

Communities of Interest

  • Materials and Manufacturing Processes
  • Weapons Technologies

DTIC Thesaurus Topics

  • Aircrafts
  • Airframes
  • Automata
  • Computer Science
  • Computers
  • Correlators
  • Distributed Computing
  • Embedded Systems
  • Language
  • Life Cycles
  • Middleware
  • Military Aircraft
  • Model Based Systems Engineering
  • Multithreading
  • Natural Languages
  • Simulations
  • Specifications

Fields of Study

  • Computer science
  • Engineering

Readers

  • Educational Psychology
  • Parallel and Distributed Computing.
  • Software Engineering.

Technology Areas

  • Space