Synthesis of large dynamic concurrent programs from dynamic specifications

Paul C. Attie

Research output: Contribution to journalArticle

Abstract

We present two methods for synthesizing large concurrent programs from temporal logic specifications. The first method deals with finite-state concurrent programs that are static, i.e., the set of processes is fixed. It produces an infinite family of static finite-state concurrent programs. The second method deals with dynamic concurrent programs, i.e., new processes can be created and added at run-time. It produces a single dynamic concurrent program. A dynamic concurrent program may be viewed as a limiting case of an infinite family of static programs, and so the second method may be viewed as generalizing the first. Our methods are algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are “alive” at any time. We do not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding state explosion. Instead, for each interacting pair of processes, we construct (from a pair-specification) a pair-structure which embodies the interaction of the two processes. From each pair-structure, we synthesize a pair-program to coordinate the two processes. Our second method allows 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. We can thus add new behaviors, which result in new properties being satisfied, at run-time. This “incremental composition” step has complexity independent of the total number of processes; it only requires the mechanical analysis of the two processes in the pair-program, and their immediate neighbors, i.e., the other processes which they interact directly with. Thus, any state-explosion incurred is explosion in the product of only two processes. We establish “large model” theorems which show that the synthesized global program inherits correctness properties from the pair-programs.

Original languageEnglish (US)
Pages (from-to)94-147
Number of pages54
JournalFormal Methods in System Design
Volume48
Issue number1-2
DOIs
StatePublished - Apr 1 2016
Externally publishedYes

Fingerprint

Explosions
Concurrent
Synthesis
Specification
Specifications
Temporal logic
Polynomials
Explosion
Chemical analysis
Program Correctness
Polynomial Complexity
Number of Components
Temporal Logic
Automata
Limiting

Keywords

  • Concurrent program
  • Dynamic process creation
  • Formal specification
  • Model checking
  • Synthesis
  • Temporal logic

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture

Cite this

Synthesis of large dynamic concurrent programs from dynamic specifications. / Attie, Paul C.

In: Formal Methods in System Design, Vol. 48, No. 1-2, 01.04.2016, p. 94-147.

Research output: Contribution to journalArticle

@article{f0fa336e756043e9aa1819ebe8ba2973,
title = "Synthesis of large dynamic concurrent programs from dynamic specifications",
abstract = "We present two methods for synthesizing large concurrent programs from temporal logic specifications. The first method deals with finite-state concurrent programs that are static, i.e., the set of processes is fixed. It produces an infinite family of static finite-state concurrent programs. The second method deals with dynamic concurrent programs, i.e., new processes can be created and added at run-time. It produces a single dynamic concurrent program. A dynamic concurrent program may be viewed as a limiting case of an infinite family of static programs, and so the second method may be viewed as generalizing the first. Our methods are algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are “alive” at any time. We do not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding state explosion. Instead, for each interacting pair of processes, we construct (from a pair-specification) a pair-structure which embodies the interaction of the two processes. From each pair-structure, we synthesize a pair-program to coordinate the two processes. Our second method allows 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. We can thus add new behaviors, which result in new properties being satisfied, at run-time. This “incremental composition” step has complexity independent of the total number of processes; it only requires the mechanical analysis of the two processes in the pair-program, and their immediate neighbors, i.e., the other processes which they interact directly with. Thus, any state-explosion incurred is explosion in the product of only two processes. We establish “large model” theorems which show that the synthesized global program inherits correctness properties from the pair-programs.",
keywords = "Concurrent program, Dynamic process creation, Formal specification, Model checking, Synthesis, Temporal logic",
author = "Attie, {Paul C.}",
year = "2016",
month = "4",
day = "1",
doi = "10.1007/s10703-016-0252-9",
language = "English (US)",
volume = "48",
pages = "94--147",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "1-2",

}

TY - JOUR

T1 - Synthesis of large dynamic concurrent programs from dynamic specifications

AU - Attie, Paul C.

PY - 2016/4/1

Y1 - 2016/4/1

N2 - We present two methods for synthesizing large concurrent programs from temporal logic specifications. The first method deals with finite-state concurrent programs that are static, i.e., the set of processes is fixed. It produces an infinite family of static finite-state concurrent programs. The second method deals with dynamic concurrent programs, i.e., new processes can be created and added at run-time. It produces a single dynamic concurrent program. A dynamic concurrent program may be viewed as a limiting case of an infinite family of static programs, and so the second method may be viewed as generalizing the first. Our methods are algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are “alive” at any time. We do not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding state explosion. Instead, for each interacting pair of processes, we construct (from a pair-specification) a pair-structure which embodies the interaction of the two processes. From each pair-structure, we synthesize a pair-program to coordinate the two processes. Our second method allows 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. We can thus add new behaviors, which result in new properties being satisfied, at run-time. This “incremental composition” step has complexity independent of the total number of processes; it only requires the mechanical analysis of the two processes in the pair-program, and their immediate neighbors, i.e., the other processes which they interact directly with. Thus, any state-explosion incurred is explosion in the product of only two processes. We establish “large model” theorems which show that the synthesized global program inherits correctness properties from the pair-programs.

AB - We present two methods for synthesizing large concurrent programs from temporal logic specifications. The first method deals with finite-state concurrent programs that are static, i.e., the set of processes is fixed. It produces an infinite family of static finite-state concurrent programs. The second method deals with dynamic concurrent programs, i.e., new processes can be created and added at run-time. It produces a single dynamic concurrent program. A dynamic concurrent program may be viewed as a limiting case of an infinite family of static programs, and so the second method may be viewed as generalizing the first. Our methods are algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are “alive” at any time. We do not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding state explosion. Instead, for each interacting pair of processes, we construct (from a pair-specification) a pair-structure which embodies the interaction of the two processes. From each pair-structure, we synthesize a pair-program to coordinate the two processes. Our second method allows 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. We can thus add new behaviors, which result in new properties being satisfied, at run-time. This “incremental composition” step has complexity independent of the total number of processes; it only requires the mechanical analysis of the two processes in the pair-program, and their immediate neighbors, i.e., the other processes which they interact directly with. Thus, any state-explosion incurred is explosion in the product of only two processes. We establish “large model” theorems which show that the synthesized global program inherits correctness properties from the pair-programs.

KW - Concurrent program

KW - Dynamic process creation

KW - Formal specification

KW - Model checking

KW - Synthesis

KW - Temporal logic

UR - http://www.scopus.com/inward/record.url?scp=84976385664&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84976385664&partnerID=8YFLogxK

U2 - 10.1007/s10703-016-0252-9

DO - 10.1007/s10703-016-0252-9

M3 - Article

AN - SCOPUS:84976385664

VL - 48

SP - 94

EP - 147

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

IS - 1-2

ER -