Algorithms for synthesizing priorities in component-based systems

DOI10.1007/978-3-642-24372-1_12zbMATH Open1348.68160arXiv1107.1383OpenAlexW1821461427MaRDI QIDQ3172911FDOQ3172911

Authors: Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Rueß, Christian Buckl, Alois Knoll 

Publication date: 7 October 2011

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Abstract: We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis.

Full work available at URL: https://arxiv.org/abs/1107.1383

Recommendations

• On the hardness of priority synthesis
• Building distributed controllers for systems with priorities
• Formal Methods for Components and Objects
• Synthesis from Component Libraries
• Dependency-Based Compositional Synthesis

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (5)

• A method for the automatic deduction of priority lists of entities and tasks from the design knowledge
• Building distributed controllers for systems with priorities
• On the hardness of priority synthesis
• Title not available (Why is that?)
• Formal Methods for Components and Objects

Uses Software

• D-Finder
• SYNTHESIS
• SPIN
• NuSMV

This page was built for publication: Algorithms for synthesizing priorities in component-based systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172911)