NDLI: Dependability Analysis for AADL Models by PVS

Content Provider	IEEE Xplore Digital Library
Author	Geng Chen Lei Luo Rong Gong Shenglin Gui
Copyright Year	2009
Abstract	In recent years, Architecture Analysis & Design Language (AADL) has been applied to the development of dependable real-time systems, in which the quality of the developed software is an important factor. Thus, to make sure that real-time systems are really dependable, we must verify the important properties, such as safety and reliability. This paper describes a contribution to the transformation of AADL models. In this paper we present an approach for transforming AADL model into Prototype Verification System (PVS) specification and deductive verification of such AADL models using the PVS interactive theorem prover. Our transformation includes two aspects: structure and behavior description. Applying a PVS specification of a AADL language semantics, we generate a formal representation of the AADL model. After the transformation, some properties, such as safety and reliability, of the model build by AADL could be verified using PVS. We use an example to demonstrate the correctness and feasibility of our approach. Then, we verified the safety and reliability attributes of dependability in our model. At last, we conclude our paper by proposing that model transformation provides powerful support to improve the integration of formal verification in an industrial engineering process and we presented our future work direction.
Starting Page	19
Ending Page	24
File Size	222572
Page Count	6
File Format	PDF
ISBN	9780769539294
e-ISBN	9781424454211
DOI	10.1109/DASC.2009.45
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2009-12-12
Publisher Place	China
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Real time systems Software prototyping dependability analysis Aerospace electronics PVS Power system modeling Automotive engineering Computer science Design engineering AADL Computer architecture Software quality Safety transforming rules
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

UCaS: A Schedulability Analysis Tool for AADL Models

Embedded real-time system modeling and analysis using AADL

Aircraft integration real-time simulator modeling with AADL for architecture tradeoffs

ArcheOpterix: An extendable tool for architecture optimization of AADL models

Formal Schedulability Analysis and Simulation for AADL

Architecture description languages for high-integrity real-time systems

ASIIST: Application Specific I/O Integration Support Tool for Real-Time Bus Architecture Designs

Virtual prototyping AADL architectures in a polychronous model of computation

The SAE Architecture Analysis & Design Language (AADL) a standard for engineering performance critical systems

Dependability Analysis for AADL Models by PVS

Similar Documents

UCaS: A Schedulability Analysis Tool for AADL Models

Embedded real-time system modeling and analysis using AADL

Aircraft integration real-time simulator modeling with AADL for architecture tradeoffs

ArcheOpterix: An extendable tool for architecture optimization of AADL models

Formal Schedulability Analysis and Simulation for AADL

Architecture description languages for high-integrity real-time systems

ASIIST: Application Specific I/O Integration Support Tool for Real-Time Bus Architecture Designs

Virtual prototyping AADL architectures in a polychronous model of computation

The SAE Architecture Analysis & Design Language (AADL) a standard for engineering performance critical systems

Dependability Analysis for AADL Models by PVS