Search NASA⌕ Search
Home/Archive/NASA NTRS

NASA NTRS · 20150021848

Assume-Guarantee Abstraction Refinement Meets Hybrid Systems

Bogomolov, Sergiy·Frehse, Goran·Greitschus, Marius·Grosu, Radu·Pasareanu, Corina S.·Podelski, Andreas·Strump, Thomas
View original source ↗Export metadata ↓

Abstract

Compositional verification techniques in the assume- guarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions we introduce an abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata.

Explore related subjects

ReliabilityStatistical MethodsModel Checking

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Bogomolov, Sergiy, Frehse, Goran, Greitschus, Marius, Grosu, Radu, Pasareanu, Corina S., Podelski, Andreas, Strump, Thomas. 2014-11-18. Assume-Guarantee Abstraction Refinement Meets Hybrid Systems. https://ntrs.nasa.gov/citations/20150021848

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRS2018

Cracking Problems and Mechanical Characteristics of PME and BME Ceramic Capacitors

Most failures in MLCCs are caused by cracking that create shorts between opposite electrodes of the parts. A use of manual soldering makes this problem especially serious for space industry. Experience shows that different lots of ceramic capacitors might have different susceptibility to cracking under manual soldering conditions. This simulates a search of techniques that would allow revealing capacitors that are most robust to soldering-induced stresses. Currently, base metal electrode (BME) capacitors are introduced to high-reliability applications as a replacement of precious metal electrode (PME) parts. Understanding the difference in the susceptibility to cracking between PME and BME capacitors would facilitate this process. This presentation gives a review of mechanical characteristics measured in-situ on MLCCs that includes flexural strength, Vickers hardness, indentation fracture toughness, and the board flex testing and compare characteristics of BME and PME capacitors. A history case related to cracking in PME capacitors that caused flight system malfunctions and mechanisms of failure are considered. Possible qualification tests that would allow evaluation of the resistance of MLCCs to manual soldering are suggested and perspectives related to introduction of BME capacitors discussed.

Reliability↗
NASA NTRS2016

Printed Circuit Board Quality Assurance

PCB Assurance Summary: PCB assurance actives are informed by risk in context of the Project. Lessons are being applied across Projects for continuous improvements. Newer component technologies, smaller/high pitch devices: tighter and more demanding PCB designs: Identifying new research areas. New materials, designs, structures and test methods.

Reliability↗
NASA NTRS2016

The NASA Electronic Parts and Packaging (NEPP) Program: NEPP Overview - Automotive Electronics

The results of NASAs studies into the appropriateness of using U.S. Automotive electronic parts in NASA spaceflight systems will be presented. The first part of the presentation provides an overview of the United States Automotive Electronics Council's AECQ standardization program, the second part provides a summary of the results of NASA's procurement and testing experiences and other lessons learned along with preliminary test results.

Reliability↗