Compositional adjustment of concurrent programs to satisfy temporal logic constraints in MENDELS ZONE

Naoshi Uchihira, Shinichi Honiden

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

In this paper, we examine "program adjustment", a formal and practical approach to developing correct concurrent programs, by automatically adjusting an imperfect program to satisfy given constraints. A concurrent program is modeled by a finite state process, and program adjustment to satisfy temporal logic constraints is formalized as the synthesis of an arbiter process which partially serializes target (i.e., imperfect) processes to remove harmful nondeterministic behaviors. Compositional adjustment is also proposed for large-scale compound target processes, using process equivalence theory. We have developed a computer-aided programming environment on the parallel computer Multi-PSI, called MENDELS ZONE, that adopts this compositional adjustment. Adjusted programs can be compiled into the kernel language (KL1) and executed on Multi-PSI.

Original languageEnglish
Pages (from-to)207-221
Number of pages15
JournalJournal of Systems and Software
Volume33
Issue number3 SPEC. ISS.
DOIs
Publication statusPublished - 1996 Jun 1
Externally publishedYes

Fingerprint

Temporal logic
Computer programming

ASJC Scopus subject areas

  • Software
  • Information Systems
  • Hardware and Architecture

Cite this

Compositional adjustment of concurrent programs to satisfy temporal logic constraints in MENDELS ZONE. / Uchihira, Naoshi; Honiden, Shinichi.

In: Journal of Systems and Software, Vol. 33, No. 3 SPEC. ISS., 01.06.1996, p. 207-221.

Research output: Contribution to journalArticle

@article{41995a863c89490090e1e33cd014e9af,
title = "Compositional adjustment of concurrent programs to satisfy temporal logic constraints in MENDELS ZONE",
abstract = "In this paper, we examine {"}program adjustment{"}, a formal and practical approach to developing correct concurrent programs, by automatically adjusting an imperfect program to satisfy given constraints. A concurrent program is modeled by a finite state process, and program adjustment to satisfy temporal logic constraints is formalized as the synthesis of an arbiter process which partially serializes target (i.e., imperfect) processes to remove harmful nondeterministic behaviors. Compositional adjustment is also proposed for large-scale compound target processes, using process equivalence theory. We have developed a computer-aided programming environment on the parallel computer Multi-PSI, called MENDELS ZONE, that adopts this compositional adjustment. Adjusted programs can be compiled into the kernel language (KL1) and executed on Multi-PSI.",
author = "Naoshi Uchihira and Shinichi Honiden",
year = "1996",
month = "6",
day = "1",
doi = "10.1016/0164-1212(96)00021-0",
language = "English",
volume = "33",
pages = "207--221",
journal = "Journal of Systems and Software",
issn = "0164-1212",
publisher = "Elsevier Inc.",
number = "3 SPEC. ISS.",

}

TY - JOUR

T1 - Compositional adjustment of concurrent programs to satisfy temporal logic constraints in MENDELS ZONE

AU - Uchihira, Naoshi

AU - Honiden, Shinichi

PY - 1996/6/1

Y1 - 1996/6/1

N2 - In this paper, we examine "program adjustment", a formal and practical approach to developing correct concurrent programs, by automatically adjusting an imperfect program to satisfy given constraints. A concurrent program is modeled by a finite state process, and program adjustment to satisfy temporal logic constraints is formalized as the synthesis of an arbiter process which partially serializes target (i.e., imperfect) processes to remove harmful nondeterministic behaviors. Compositional adjustment is also proposed for large-scale compound target processes, using process equivalence theory. We have developed a computer-aided programming environment on the parallel computer Multi-PSI, called MENDELS ZONE, that adopts this compositional adjustment. Adjusted programs can be compiled into the kernel language (KL1) and executed on Multi-PSI.

AB - In this paper, we examine "program adjustment", a formal and practical approach to developing correct concurrent programs, by automatically adjusting an imperfect program to satisfy given constraints. A concurrent program is modeled by a finite state process, and program adjustment to satisfy temporal logic constraints is formalized as the synthesis of an arbiter process which partially serializes target (i.e., imperfect) processes to remove harmful nondeterministic behaviors. Compositional adjustment is also proposed for large-scale compound target processes, using process equivalence theory. We have developed a computer-aided programming environment on the parallel computer Multi-PSI, called MENDELS ZONE, that adopts this compositional adjustment. Adjusted programs can be compiled into the kernel language (KL1) and executed on Multi-PSI.

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

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

U2 - 10.1016/0164-1212(96)00021-0

DO - 10.1016/0164-1212(96)00021-0

M3 - Article

AN - SCOPUS:0030165810

VL - 33

SP - 207

EP - 221

JO - Journal of Systems and Software

JF - Journal of Systems and Software

SN - 0164-1212

IS - 3 SPEC. ISS.

ER -