Algorithms for synthesizing priorities in component-based systems

DOI10.1007/978-3-642-24372-1_12MaRDI QIDQ3172911zbMATHOpenAlexFDO

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)

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

Mathematics Subject Classification ID

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

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.

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

Cited in

(5)

• Building distributed controllers for systems with priorities
• Formal Methods for Components and Objects
• A method for the automatic deduction of priority lists of entities and tasks from the design knowledge
• scientific article; zbMATH DE number 1759390 (Why is no real title available?)
• On the hardness of priority synthesis

Describes a project that uses

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)