Скачать 0.98 Mb.
In the area of mathematical modeling the most important general de-facto standards for different dynamic simulation modes are:
The insufficient power and generality of the former modeling languages stimulated the development of Modelica (as a true object-oriented, multi-physics language) and VHDL-AMS/Verilog-AMS (multi-physics but strongly influenced by electronics).
The rapid increase in new requirements to handle the dynamics of highly complex, heterogeneous systems requires enhanced efforts in developing new language features (based on existing languages!). Especially the efficient simulation of hardware-software systems and model structural dynamics are yet unsolved problems. In electronics and telecommunications, therefore, the development of SystemC-AMS has been launched but these attempts are far from the multi-physics and multi-domain applications which are addressed by Modelica.
gProms (general Process Modeling Systems) (Min and Pantelides 1996 ) provides a set of advanced tools for supporting model development and maintenance. Several techniques are provided for model validation, dynamic optimization, optimal experiment design, and life cycle modeling, but unfortunately gProms lacks support for debugging simulation models when structural or numerical failures occur.
VHDL-AMS (Christen and Bakalar 1999 ) is the IEEE-endorsed standard modeling language (standard 1076.1) created to provide a general-purpose, easily exchangeable and open language for modern analog-mixed-signal designs. Models can be exchanged between all simulation tools that adhere to the VHDL-AMS standard. Advantages of VHDL-AMS are:
The χ language (Fábián 1999 ) is a hybrid specification formalism, suitable for the description of discrete-event, continuous-time, and hybrid systems. It is a concurrent language, where the discrete-event part is based on Communicating Sequential Processes (Hoare 1985 ) and the continuous-time part is based on Differential Algebraic Equations (DAEs). Models written in the χ language can be executed by the χ simulator.
Concerning specification languages for programming language semantics, compiler generators based on denotational semantics (Pettersson and Fritzson 1992 ) (Ringström et al. 1994 ), have been investigated and developed with some success. However this formalism has certain usability problems, and Operational Semantics/Natural Semantics has become the dominant formalism in common language semantics specification literature.
Therefore a meta-language and compiler generator called RML (Relational Meta Language) (Fritzson 1998 , PELAB 1994-2008 , Pettersson 1995 , Pettersson 1999 ) for Natural Semantics was developed, which we have used extensively for full-scale specifications of languages like Java 1.2 (Holmén 2000 ), C subset with pointer arithmetic, functional, and equation-based object-oriented languages (Modelica). Generated implementations are comparable in performance to hand implementations. However, it turned out that development environment support is needed also for specification languages. Recent developments include a debugger for Natural Semantics specifications (Pop and Fritzson 2005 ) and (Chapter 7).
Natural Semantics (Kahn 1988 ) is a specification formalism that is used to specify the semantics of programming languages, i.e., type systems, dynamic semantics, translational semantics, static semantics (Despeyroux 1984 , Glesner and Zimmermann 2004 ), etc. Natural Semantics is an operational semantics derived from the Plotkin (Plotkin 1981 ) structural operational semantics combined with the sequent calculus for natural deduction. There are few systems implemented that compile or interpret Natural Semantics.
One of these systems is Centaur (Borras et al. 1988 ) with its implementation of Natural Semantics called Typol (Despeyroux 1984 , Despeyroux 1988 ). This system is translating the Natural Semantics inference rules to Prolog.
The Relational Meta-Language (RML) is an efficient implementation of Natural Semantics, with a performance of the generated code that is several orders of magnitude better than Typol. The RML language is compiled to highly efficient C code by the rml2c compiler. In this way large parts of a compiler can be automatically generated from their Natural Semantics specifications. RML is successfully used for specifying and generating practically usable compilers from Natural Semantics for Java, Modelica, MiniML (Clément et al. 1986 ), Mini-Freja (Pettersson 1995 ) and other languages.
As a simple example of using Natural Semantics and the Relational Meta-Language (RML) we present a trivial expression (Exp1) language and its specification in Natural Semantics and RML. A specification in Natural Semantics has two parts:
In our example language we have expressions built from numbers. The abstract syntax of this language is declared in the following way:
The inference rules for our language are bundled together in a judgment in the following way (here we do not present similar rules for the other operators.):
RML modules have two parts, an interface comprising datatype declarations (abstract syntax) and signatures of relations (judgments) that operate on such datatypes, followed by the declarations of the actual relations which group together rules and axioms. In RML, the Natural Semantics specification shown above is represented as follows:
(* Abstract syntax of the language Exp1 *)
datatype Exp = RCONST of real
| ADD of Exp * Exp
| SUB of Exp * Exp
| MUL of Exp * Exp
| DIV of Exp * Exp
| NEG of Exp
relation eval: Exp => real
(* Evaluation semantics of Exp1 *)
relation eval: Exp => real =
(* Evaluation of a real node is the real number itself *)
axiom eval(RCONST(rval)) => rval
(* Evaluation of an addition node ADD is v3, if v3 is
the result of adding the evaluated results of its
children e1 and e2. *)
rule eval(e1) => v1 & eval(e2) => v2 & v1 + v2 => v3
eval( ADD(e1, e2) ) => v3
rule eval(e1) => v1 & eval(e2) => v2 & v1 - v2 => v3
eval( SUB(e1, e2) ) => v3
rule eval(e1) => v1 & eval(e2) => v2 & v1 * v2 => v3
eval( MUL(e1, e2) ) => v3
rule eval(e1) => v1 & eval(e2) => v2 & v1 / v2 => v3
eval( DIV(e1, e2) ) => v3
rule eval(e) => v & -v => vneg
eval( NEG(e) ) => vneg
end (* eval *)
A proof-theoretic interpretation can be assigned to this specification. We interpret inference rules as recipes for constructing proofs. We wish to prove that there is a value such that holds for this specification. To prove this proposition we need an inference rule that has a conclusion, which can be instantiated (matched) to the proposition. The only proposition that matches is the second proposition (2), which is instantiated as follows:
To continue the proof, we need to apply the first proposition (axiom) several times, and we soon reach the conclusion. One can observe that debugging of Natural Semantics comprise proof-tree understanding.
Regarding the specification of lexical and syntatic rules for a new language, we use external tools such as Lex, Yacc, Flex, Bison, etc., to generate those modules. The parser builds abstract syntax by calling RML-defined constructors. The abstract syntax is then passed from the parser to the RML-generated modules. We currently use the same approach for languages defined using MetaModelica.
The SOSDT (Structural Operational Semantics Development Tooling) is an integrated environment for RML (Figure 2 -13).
Figure 2 13. SOSDT Eclipse Plugin for RML Development.
The SOSDT environment (Pop and Fritzson 2006 ) includes support for browsing, code completion through menus or popups, code checking, automatic indentation, and debugging of specifications.
|The Domain Analysis Integrated in an Object Oriented Development Methodology||Hypergraph-based Object-oriented Model for gis application|
|Object-Oriented Object-Oriented Languages||Applying uml and Patterns: An Introduction to Object-Oriented Analysis and Design and Iterative Development (3rd Edition)|
|Model Development of a Total Integrated Maintenance System||An integrated framework for model-based flow assurance in deep-water oil and gas production|
|This paper introduces the basic concepts of Agile Database Techniques, and effective ways to go about the Data-Oriented aspects of Object Oriented software||Object-Oriented Metrics: an Annotated Bibliography|
|An Introduction and Brief Examination of Object-Oriented Data Modeling||An Object-Oriented Support Tool for the Design of Casting Procedures|