TY - JOUR
T1 - Compositional adjustment of concurrent programs to satisfy temporal logic constraints in MENDELS ZONE
AU - Uchihira, Naoshi
AU - Honiden, Shinichi
N1 - Funding Information:
This research has been supported by ICOT, and we would like to thank the members of that organization. We are also grateful to Sadakazu Watanabe and Kazuo Matsumura of the Systems & Software Engineering Laboratory, Toshiba Corporation, for providing support throughout this work.
PY - 1996/6
Y1 - 1996/6
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
SN - 0164-1212
VL - 33
SP - 207
EP - 221
JO - Journal of Systems and Software
JF - Journal of Systems and Software
IS - 3 SPEC. ISS.
ER -