zhensong's functional_models [5 articles]

Abstract

Beginning with a bounded (safe), live, or reversible Petri net as a first-level net model for a system, Petri nets are synthesized by first refining operation places through basic design modules in top-down modular ways, then adding nonshared resource places stepwise, and finally adding shared resource places step by step in a bottom-up manner. Refinement theory is extended to include reversibility of Petri nets. Parallel and sequential mutual exclusions are used to model shared resources. Design of the first-level Petri nets ...

Abstract

Embedded systems have been a traditional area of strength in the research agenda of the University of California at Berkeley. In parallel to this effort, a pattern of graduate and undergraduate classes has emerged that is the result of a distillation process of the research results. In this paper, we present the considerations that are driving our curriculum development and we review our undergraduate and graduate program. In particular, we describe in detail a graduate class (EECS249: Design of Embedded Systems: ...

Abstract

The main purpose of this paper is to present how the Unified Modeling Language (UML) can be used for modeling industrial embedded systems. By using a car radios production line as a running example, the paper demonstrates the modeling process that can be followed during the analysis phase of complex control applications. In order to guarantee the continuity mapping of the models, the authors propose some guidelines to transform the use case diagrams into a single object diagram, which is one ...

Abstract

Flight software is the central nervous system of modern spacecraft. Verifying spacecraft flight software to assure that it operates correctly and safely is presently an intensive and costly process. A multitude of scenarios and tests must be devised, executed and reviewed to provide reasonable confidence that the software will perform as intended and not endanger the spacecraft. Undetected software defects on spacecraft and launch vehicles have caused embarrassing and costly failures in recent years. Model checking is a technique for software ...