Synthesis of large dynamic concurrent programs from dynamic specifications
From MaRDI portal
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: We present a tractable method for synthesizing arbitrarily large concurrent programs, for a shared memory model with common hardware-available primitives such as atomic registers, compare-and-swap, load-linked/store conditional, etc. The programs we synthesize are dynamic: new processes can be created and added at run-time, and so our programs are not finite-state, in general. Nevertheless, we successfully exploit automatic synthesis and model-checking methods based on propositional temporal logic. Our method is algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are ``alive at any time. Our method does not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding intr{state explosion}. Instead, for each pair of processes which interact, our method constructs an automata-theoretic product (intr{pair-machine}) which embodies all the possible interactions of these two processes. From each pair-machine, we can synthesize a correct intr{pair-program} which coordinates the two involved processes as needed. We allow such pair-programs to be added dynamically at run-time. They are then ``composed conjunctively with the currently alive pair-programs to re-synthesize the program as it results after addition of the new pair-program. We are thus able to add new behaviors, which result in new properties being satisfied, at run-time. We establish a ``large model theorem which shows that the synthesized large program inherits correctness properties from the pair-programs.
Recommendations
Cites work
- scientific article; zbMATH DE number 1614699 (Why is no real title available?)
- scientific article; zbMATH DE number 1701752 (Why is no real title available?)
- scientific article; zbMATH DE number 996442 (Why is no real title available?)
- scientific article; zbMATH DE number 3784244 (Why is no real title available?)
- scientific article; zbMATH DE number 177523 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 1032897 (Why is no real title available?)
- scientific article; zbMATH DE number 1759605 (Why is no real title available?)
- scientific article; zbMATH DE number 1796136 (Why is no real title available?)
- A framework for automated distributed implementation of component-based models
- Abstract Model Repair
- An axiomatic basis for computer programming
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Bounded Synthesis
- Characterizing finite Kripke structures in propositional temporal logic
- Computer Aided Verification
- Decidability of parameterized verification
- Depth-First Search and Linear Graph Algorithms
- Dynamic input/output automata: a formal and compositional model for dynamic systems
- Enhancing model checking in verification by AI techniques
- Eventually-serializable data services
- Finite-state concurrent programs can be expressed in pairwise normal form
- Latticed-LTL synthesis in the presence of noisy inputs
- Modalities for model checking: Branching time logic strikes back
- Reasoning about networks with many identical finite state processes
- Reasoning about systems with many processes
- Self-stabilizing systems in spite of distributed control
- Symbolic synthesis of masking fault-tolerant distributed programs
- Synthesis from Component Libraries
- Synthesis from component libraries with costs
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Synthesis of concurrent systems for an atomic read/atomic write model of computation
- Synthesis of fault-tolerant concurrent programs
- Temporal verification of reactive systems: response
- Using branching time temporal logic to synthesize synchronization skeletons
- Verification, Model Checking, and Abstract Interpretation
Cited in
(10)- Modular verification of interactive systems with an application to biology
- Synthesizing concurrent programs using answer set programming
- scientific article; zbMATH DE number 5149070 (Why is no real title available?)
- Synthesis of a system composed by many similar objects
- scientific article; zbMATH DE number 177266 (Why is no real title available?)
- scientific article; zbMATH DE number 3868590 (Why is no real title available?)
- Finite-state concurrent programs can be expressed in pairwise normal form
- Abstract Semantic Diffing of Evolving Concurrent Programs
- An algorithmic framework for synthesis of concurrent programs
- scientific article; zbMATH DE number 3976309 (Why is no real title available?)
This page was built for publication: Synthesis of large dynamic concurrent programs from dynamic specifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q346790)
