Synthesis of large dynamic concurrent programs from dynamic specifications

DOI10.1007/S10703-016-0252-9zbMATH Open1392.68143arXiv0801.1687OpenAlexW1677924248MaRDI QIDQ346790FDOQ346790

Authors: Paul C. Attie 

Publication date: 30 November 2016

Published in: Formal Methods in System Design (Search for Journal in Brave)

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.

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

Recommendations

• scientific article; zbMATH DE number 1361120
• An algorithmic framework for synthesis of concurrent programs
• Synthesizing concurrent programs using answer set programming
• scientific article; zbMATH DE number 177266
• scientific article; zbMATH DE number 177523

zbMATH Keywords

synthesismodel checkingtemporal logicconcurrent programdynamic process creationformal specification

Mathematics Subject Classification ID

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)

Cites Work

• Computer Aided Verification
• Characterizing finite Kripke structures in propositional temporal logic
• Title not available (Why is that?)
• Reasoning about systems with many processes
• Title not available (Why is that?)
• Depth-First Search and Linear Graph Algorithms
• Reasoning about networks with many identical finite state processes
• Title not available (Why is that?)
• Self-stabilizing systems in spite of distributed control
• Title not available (Why is that?)
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Using branching time temporal logic to synthesize synchronization skeletons
• Temporal verification of reactive systems: response
• Title not available (Why is that?)
• Synthesis from component libraries with costs
• Eventually-serializable data services
• Enhancing model checking in verification by AI techniques
• Modalities for model checking: Branching time logic strikes back
• Symbolic synthesis of masking fault-tolerant distributed programs
• A framework for automated distributed implementation of component-based models
• Dynamic input/output automata: a formal and compositional model for dynamic systems
• Title not available (Why is that?)
• Synthesis of fault-tolerant concurrent programs
• Synthesis of concurrent systems for an atomic read/atomic write model of computation
• Abstract Model Repair
• Bounded Synthesis
• Synthesis from Component Libraries
• Synthesis of Communicating Processes from Temporal Logic Specifications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Decidability of parameterized verification
• Latticed-LTL synthesis in the presence of noisy inputs
• Verification, Model Checking, and Abstract Interpretation
• Finite-state concurrent programs can be expressed in pairwise normal form

Cited In (10)

• An algorithmic framework for synthesis of concurrent programs
• Synthesizing concurrent programs using answer set programming
• Title not available (Why is that?)
• Abstract Semantic Diffing of Evolving Concurrent Programs
• Synthesis of a system composed by many similar objects
• Title not available (Why is that?)
• Title not available (Why is that?)
• Finite-state concurrent programs can be expressed in pairwise normal form
• Modular verification of interactive systems with an application to biology
• Title not available (Why is that?)

Uses Software

• SyncGen

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)