Formal derivation of rule-based programs

Author

Roma, G.-C. ; Gamble, Rose F. ; Ball, William E.

Author_Institution

Dept. of Comput. Sci., Washington Univ., St. Louis, MO, USA

Volume

19

Issue

3

fYear

1993

fDate

3/1/1993 12:00:00 AM

Firstpage

277

Lastpage

296

Abstract

It is shown that a combination of specification and program refinement may be applied to deriving efficient concurrent rule-based programs. Specification refinement is used to generate an initial rule-based program that is refined into a program which is highly concurrent and efficient. This program derivation strategy is divided into two major tasks. The first task relies on specification refinement. Techniques similar to those employed in the derivation of UNITY programs are used to produce a correct rule-based program having a static knowledge base. The second task involves program refinement and is specific to the development of concurrent rule-based programs. It relies heavily on the availability of a computational model, such as Swarm, that has the ability to dynamically restructure the knowledge base. The ways in which a Swarm program can be translated to OPS5 specifically, given some restrictions, while maintaining the correctness criteria are discussed

Keywords

formal specification; knowledge based systems; logic programming; parallel programming; OPS5; Swarm; UNITY programs; computational model; correct rule-based program; correctness criteria; efficient concurrent rule-based programs; initial rule-based program; program derivation strategy; program refinement; specification refinement; static knowledge base; Concurrent computing; Expert systems; Formal specifications; Formal verification; Hardware; Logic programming; Parallel algorithms; Parallel processing; Parallel programming; Refining;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.221138

Filename

221138