Design and specification of embedded systems in Java using successive, formal refinement

Abstract

Successive, formal refinement is a new approach for specificationof embedded systems using a general-purpose programming language.Systems are formally modeled as Abstractable SynchronousReactive systems, and Java is used as the design inputlanguage. A policy of use is applied to Java, in the form of languageusage restrictions and class-library extensions, to ensureconsistency with the formal model. A process of incremental,user-guided program transformation is used to refine a Java programuntil it is consistent with the policy of use. The final productis a system specification possessing the properties of the formalmodel, including deterministic behavior, bounded memory usage,and bounded execution time. This approach allows systems designto begin with the flexibility of a general-purpose language, followedby gradual refinement into a more restricted form necessaryfor specification.