Design and Specification of Embedded Systems in Java Using Successive, Formal Refinement

Successive, formal refinement is a new approach for specification of embedded systems using a general-purpose programming language. Systems are formally modeled as Abstractable Synchronous Reactive systems, and Java is used as the design input language. A policy of use is applied to Java, in the form of language usage restrictions and class-library extensions, to ensure consistency with the formal model. A process of incremental, user-guided program transformation is used to refine a Java program until it is consistent with the policy of use. The final product is a system specification possessing the properties of the formal model, including deterministic behavior, bounded memory usage, and bounded execution time. This approach allows systems design to begin with the flexibility of a general-purpose language, followed by gradual refinement into a more restricted form necessary for specification.

• Type: Conference
• Year: 1998
• Where: DAC
• Authors: James Shin Young, Josh MacDonald, Michael Shilman, Abdallah Tabbara, Paul N. Hilfinger, A. Richard Newton
• Keywords: DAC 1998, Design Automation, Formal Refinement, General-purpose Programming Language, Language Usage Restrictions