Formal models for systems prototyping

The long process of systems development starts with the identification of a problem and the analysis of its requirements. This is an important phase, crucial to the eventual development of an implementation. At this stage the intended behaviour of the system should be well understood and discussed between users and implements. A representation of the requirements is done using a model that serves as a communication document and as a guide for the development. This thesis proposes a methodology to prototype models of systems at the requirements analysis phase. Our main concern is to bring formality both to this level and to the tools and process of development. This methodology starts with the use of a widely known graphic representation, Data Flow Diagrams, and a path is followed until an executable prototype is reached. This path proposes the use of Predicate/Transition Nets as a second step, introducing detail about the behaviour of the system. The prototyping of the models represented with nets is achieved using an object-based concurrent language. The prototype in this language is automatically translated from the nets representation. Every tool used has its semantics formally defined and every step in the methodology is proved to maintain the meaning of the model. Two major real problems have been used to demonstrate the use of the proposed methodology.