• 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-05-23
One promising solution for increasing vehicle fuel economy, while still maintaining long-range driving capability, is the plug-in hybrid electric vehicle (PHEV). A PHEV is a hybrid electric vehicle (HEV) whose rechargeable energy source can be recharged from an external power source, making it a combination of an electric vehicle and a traditional hybrid vehicle. A PHEV is capable of operating as an electric vehicle until the battery is almost depleted, at which point the on-board internal combustion engine turns on, and generates power to meet the vehicle demands. When the vehicle is not in use, the battery can be recharged from an external energy source, once again allowing electric driving. A series of models is presented which simulate various powertrain architectures of PHEVs. To objectively evaluate the effect of powertrain architecture on fuel economy, the models were run according to the latest test procedures and all fuel economy values were utility factor weighted.
Video
2012-01-24
A combination of laboratory reactor measurements and vehicle FTP testing has been combined to demonstrate a method for diagnosing the formation of NO2 from a diesel oxidation catalyst (DOC). Using small cores from a production DOC and simulated diesel exhaust, the laboratory reactor experiments are used to support a model for DOC chemical reaction kinetics. The model we propose shows that the ability to produce NO2 is chemically linked to the ability of the catalyst to oxidize hydrocarbon (HC). For thermally damaged DOCs, loss of the HC oxidation function is simultaneous with loss of the NO2 production function. Since HC oxidation is the source of heat generated in the DOC under regeneration conditions, we conclude that a diagnostic of the DOC exotherm is able to detect the failure of the DOC to produce NO2. Vehicle emissions data from a 6.6 L Duramax HD pick-up with DOC of various levels of thermal degradation is provided to support the diagnostic concept.
Video
2011-12-05
These advanced checks have resulted in development of many new diagnostic monitors, of varying types, and a whole new internal software infrastructure to handle tracking, reporting, and self-verification of OBD related items. Due to this amplified complexity and the consequences surrounding a shortfall in meeting regulatory requirements, efficient and thorough validation of the OBD system in the powertrain control software is critical. Hardware-in-the-Loop (HIL) simulation provides the environment in which the needed efficiency and thoroughness for validating the OBD system can be achieved. A HIL simulation environment consisting of engine, aftertreatment, and basic vehicle models can be employed, providing the ability for software developers, calibration engineers, OBD experts, and test engineers to examine and validate both facets of OBD software: diagnostic monitors and diagnostic infrastructure (i.e., fault memory management).
Video
2012-05-23
Due to the integration of many interacting subsystems like hybrid vehicle management, energy management, distance management, etc. into the VCU platform the design steps for function development and calibration become more and more complex. This makes an aid necessary to relieve the development. Therefore, the aim of the proposed simulation-based development and calibration design is to improve the time-and-cost consuming development stages of modern VCU platforms. A simulation-based development framework is shown on a complex function development and calibration case study using an advanced powertrain concept with a plug-in hybrid electric vehicle (PHEV) concept with two electrical axles. Presenter Thomas Boehme, IAV GmbH

Related Items

Article
2016-11-15
Training / Education
2015-01-08
Technical Paper / Journal Article
2010-10-19
Technical Paper / Journal Article
2010-10-25
Technical Paper / Journal Article
2010-09-28
Training / Education
2017-08-30