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
- A framework for automated distributed implementation of component-based models
- Abstract Model Repair
- An axiomatic basis for computer programming
- Automatic deductive verification with invisible invariants
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Bounded Synthesis
- Characterizing finite Kripke structures in propositional temporal logic
- Decidability of parameterized verification
- Depth-First Search and Linear Graph Algorithms
- Dynamic input/output automata: a formal and compositional model for dynamic systems
- Efficiently verifiable conditions for deadlock-freedom of large concurrent programs
- Enhancing model checking in verification by AI techniques
- Eventually-serializable data services
- Finite-state concurrent programs can be expressed in pairwise normal form
- 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 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- Latticed-LTL synthesis in the presence of noisy inputs
- Modalities for model checking: Branching time logic strikes back
- Open systems in reactive environments: Control and synthesis
- Parameterized verification with automatically computed inductive assertions
- Reasoning about networks with many identical finite state processes
- Reasoning about systems with many processes
- Reducing model checking of the many to the few
- SAL 2
- 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
- Synthesizing processes and schedulers from temporal specifications
- Temporal verification of reactive systems: response
- Using branching time temporal logic to synthesize synchronization skeletons
- Verification of sequential and concurrent programs.
Cited in
(11)- An algorithmic framework for synthesis of concurrent programs
- scientific article; zbMATH DE number 3868590 (Why is no real title available?)
- Synthesis of a system composed by many similar objects
- scientific article; zbMATH DE number 5149070 (Why is no real title available?)
- scientific article; zbMATH DE number 3976309 (Why is no real title available?)
- scientific article; zbMATH DE number 177266 (Why is no real title available?)
- Synthesis of large concurrent programs via pairwise composition
- Synthesizing concurrent programs using answer set programming
- Abstract Semantic Diffing of Evolving Concurrent Programs
- Modular verification of interactive systems with an application to biology
- Finite-state concurrent programs can be expressed in pairwise normal form
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)
