• Video
  • 21-Mar-2012 09:50 EDT

Integrating Formal Model Checking with the RTEdge™ AADL Microkernel

00:26:21
Length:

Purchase Required to View Video

Short Preview Below

Edgewater Computer Systems Inc. product RTEdge Platform 1.2 is a software toolset supporting proof based engineering, implementation and deployment of software components, built using the RTEdge AADL Microkernel modeling subset. This is a small subset of the AADL component model and execution semantics, covering threads and thread-groups communicating solely through asynchronous event ports and through explicitly shared data ports. Threads behavior is expressed as state machines and dispatch run time semantics is encoded in a Run-time Executive, enforcing pre-emptive priority dispatch based on statically assigned event priorities, with ceiling priority protocol access to shared data. This simple AADL microkernel semantic core can support all dispatch policies, communication and synchronization mechanisms of a fully fledged AADL run time environment, permitting the systematic use of the RTEdge static analysis tools for AADL compliant software components. The objective of our work was to integrate RTEdge Platform 1.2 with the Promela / Spin model checker, for the purpose enabling formal verification of user defined formal properties, expressed on software application models built and executed on the RTEdge AADL Microkernel. In order to deal with the state space explosion problem, Model Checking relies on abstractions. Human intervention is required in an error prone process of defining the right abstractions, implementing an equivalent abstracted model in the model checker formalism, proving or disproving a property by model checking and applying the findings to the implementation. Assume-Guarantee Compositional Verification provides both a state space divide and conquer strategy and a model checking automation strategy, in a reverse engineering process applied to existing component implementations, as an iterative process of assumption refinement by model checking. The RTEdge concepts of Protocols, Capsule Interfaces and Composite Capsules open the possibility of using Assume-Guarantee contracts as a specification mechanism, in a forward engineering manner, and of verifying their consistence and conformance by the systematic use of Model Checking. Such an approach would allow verifying very large state spaces by using hierarchical component abstractions formally maintained in the RTEdge AADL component model via the extends and implements refinement relationships. To that end, Protocols, Capsule Interfaces and Composite Capsules must have a compact and convenient way of specifying sets of legal sequences of Signal Events. We developed a set of requirements for adapting IEEE1850 Property Specification Language (PSL) to formally express RTEdge software component temporal properties. The adapted PSL will use RTEdge Protocols Signals and Data as the underlying vocabulary of the PSL Boolean layer.

Presenter
Serban Gheorghe, Edgewater Computer Systems Inc.

Buy
Select
Price
List
Purchase to View
$19.00
Learn More
Technical Paper / Journal Article
2011-10-18
TECH PPR 2011 AEROTECH
Share
HTML for Linking to Page
Page URL
Grade
Rate It
No ratings yet

View More Video

Video
2012-03-21
As a result of recommendation from the Augustine Panel, the direction for Human Space Flight has been altered from the original plan referred to as Constellation. NASA's Human Exploration Framework Team (HEFT) proposes the use of a Shuttle Derived Heavy Lift Launch Vehicle (SDLV) and an Orion derived spacecraft (salvaged from Constellation) to support a new flexible direction for space exploration. The SDLV must be developed within an environment of a constrained budget and a preferred fast development schedule. Thus, it has been proposed to utilize existing assets from the Shuttle Program to speed development at a lower cost. These existing assets should not only include structures such as external tanks or solid rockets, but also the Flight Software which has traditionally been a ?long pole? in new development efforts. The avionics and software for the Space Shuttle was primarily developed in the 70's and considered state of the art for that time.
Video
2012-05-25
In support of the U.S Department of Energy's Vehicle Technologies Program, numerous vehicle technology combinations have been simulated using Autonomie. Argonne National Laboratory (Argonne) designed and wrote the Autonomie modeling software to serve as a single tool that could be used to meet the requirements of automotive engineering throughout the development process, from modeling to control, offering the ability to quickly compare the performance and fuel efficiency of numerous powertrain configurations. For this study, a multitude of vehicle technology combinations were simulated for many different vehicles classes and configurations, which included conventional, power split hybrid electric vehicle (HEV), power split plug-in hybrid electric vehicle (PHEV), extended-range EV (E-REV)-capability PHEV, series fuel cell, and battery electric vehicle.
Video
2016-10-18
Before self-driving cars are safe for public roads, a technology called "Machine Learning" will have to be far more capable than it is today. In this episode of SAE Eye on Engineering, Editor-In-Chief Lindsay Brooke looks at the challenges ahead for autonomous driving. SAE Eye on Engineering also airs Monday mornings on WJR 760 AM Detroit's Paul W. Smith Show. Access archived episodes of SAE Eye on Engineering.
Video
2012-05-22
This paper reports solubility, diffusivity and permeability data for soy and rapeseed methyl esters in polyethylene together with comparisons with methyl oleate and linoleate. These data were used to discuss the reliability of predictive models for diffusion and solubility of additive type molecules into semi-crystalline thermoplastic polymers. Presenter Emmanuel Richaud

Related Items

Training / Education
2017-09-13
Technical Paper / Journal Article
2003-11-10
Technical Paper / Journal Article
2003-10-27
Training / Education
2010-03-15
Training / Education
2015-04-06
Training / Education
2017-06-28
Technical Paper / Journal Article
2003-10-27
Technical Paper / Journal Article
2003-10-19
Video
2017-03-26