共查询到20条相似文献,搜索用时 31 毫秒
1.
Kirsten Berkenkötter Stefan Bisanz Ulrich Hannemann Jan Peleska 《International Journal on Software Tools for Technology Transfer (STTT)》2006,8(2):167-176
In this article, a new UML extension for the specification of hybrid systems, where observables may consist of both discrete
and time-continuous parameters, is presented. Whereas hybrid modeling constructs are not available in standard UML, several
specification formalisms for this type of system have been elaborated and discussed, among them the CHARON language of Alur
et al. which possesses already several attractive features for modeling embedded real-time systems with hybrid characteristics.
Adopting this as a basis, the profile inherits formal semantics based on CHARON, so it offers the possibility for formal reasoning
about hybrid UML specifications. Conversely, the CHARON framework is associated with a new syntactic representation within
the UML 2.0 world, allowing to develop hybrid specifications with arbitrary CASE tools supporting UML 2.0 and its profiling
mechanism. The “look-and-feel” of the profile is illustrated by means of a case study of an embedded system controlling the
cabin illumination in an aircraft. The benefits and weaknesses of the constructed hybrid UML profile are discussed, resulting
in feed-back for the improvement of both UML 2.0 and the CHARON formalism.
The work presented in this article has been investigated by the authors in the context of the HYBRIS (Efficient Specification
of Hybrid Systems) project supported by the Deutsche Forschungsgemeinschaft DFG as part of the priority programme on Software Specification - Integration of Software Specification Techniques for Applications in Engineering. 相似文献
2.
We develop module algebra for structured specifications with model oriented denotations. Our work extends the existing theory with specification building operators for non-protecting importation modes and with new algebraic rules (most notably for initial semantics) and upgrades the pushout-style semantics of parameterized modules to capture the (possible) sharing between the body of the parameterized modules and the instances of the parameters. We specify a set of sufficient abstract conditions, smoothly satisfied in the actual situations, and prove the isomorphism between the parallel and the serial instantiation of multiple parameters. Our module algebra development is done at the level of abstract institutions, which means that our results are very general and directly applicable to a wide variety of specification and programming formalisms that are rigorously based upon some logical system. 相似文献
3.
4.
5.
Amir A. Khwaja Author Vitae Joseph E. Urban Author Vitae 《Journal of Systems and Software》2010,83(11):2344-2362
Specification formalisms may be classified through some common properties. Specification formalism classification may be used as a basis for the evaluation of the adequacy of formal specification languages within specific application domains. System modelers may use this classification to determine if the system modeling requirements can be met by a particular class of specification formalism. This paper evaluates existing specification formalism classification approaches by various researchers and highlights certain observations regarding the suggested classification schemes. The paper then proposes a specification formalism classification method using specification language properties. The proposed classification approach, loosely following the prototype theory for classification, maps specification language properties to specification formalisms and determines which language properties can best be achieved by different formalisms. 相似文献
6.
7.
张维石 《小型微型计算机系统》1999,20(7):517-520
本文首先阐述了利用DFA模型技术进行状态转换系统描述存在的主要问题,提出了利用代数规约技术解决这些问题的可行性,然后介绍了新一代具有松散语义的代数规约语言SPECTRUM及其主要规约操作符的语法和语义,并根据DFA模型及其语言的数学定义,给出了它们的结构化代数规约,为基于DFA模型的状态转换系统的形式化设计和开发奠定了基础。 相似文献
8.
From ATP to timed graphs and hybrid systems 总被引:1,自引:0,他引:1
9.
10.
Modeling and formal verification of embedded systems based on a Petri net representation 总被引:2,自引:0,他引:2
In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications. 相似文献
11.
Message Sequence Charts (MSC) is a graphical and textual specification language developed by ITU-T. It is widely used in telecommunication software engineering for specifying behavioral scenarios. Recently, the time concept has been introduced into MSC'2000. To support the specification and verification of real-time systems using timed MSC, we need to define its formal semantics. In this paper, we use timed lposet as a semantic model and give a formal semantics for timed MSC. We first define an event in a timed MSC as a timed lposet, then give a formal semantics for timed basic MSCs, timed MSCs with structures and high-level MSCs. In this paper, we also discuss some important issues related to timed MSC. 相似文献
12.
13.
Fahiem Bacchus 《Computational Intelligence》1990,6(4):209-231
This paper presents a logical formalism for representing and reasoning with statistical knowledge. One of the key features of the formalism is its ability to deal with qualitative statistical information. It is argued that statistical knowledge, especially that of a qualitative nature, is an important component of our world knowledge and that such knowledge is used in many different reasoning tasks. The work is further motivated by the observation that previous formalisms for representing probabilistic information are inadequate for representing statistical knowledge. The representation mechanism takes the form of a logic that is capable of representing a wide variety of statistical knowledge, and that possesses an intuitive formal semantics based on the simple notions of sets of objects and probabilities defined over those sets. Furthermore, a proof theory is developed and is shown to be sound and complete. The formalism offers a perspicuous and powerful representational tool for statistical knowledge, and a proof theory which provides a formal specification for a wide class of deductive inferences. The specification provided by the proof theory subsumes most probabilistic inference procedures previously developed in AI. The formalism also subsumes ordinary first-order logic, offering a smooth integration of logical and statistical knowledge. 相似文献
14.
Till Mossakowski Serge Autexier Dieter Hutter 《The Journal of Logic and Algebraic Programming》2006,67(1-2):114
Development graphs are a tool for dealing with structured specifications in a formal program development in order to ease the management of change and reusing proofs. In this work, we extend development graphs with hiding (e.g. hidden operations). Hiding is a particularly difficult to realize operation, since it does not admit such a good decomposition of the involved specifications as other structuring operations do. We develop both a semantics and proof rules for development graphs with hiding. The rules are proven to be sound, and also complete relative to an oracle for conservative extensions. We also show that an absolutely complete set of rules cannot exist.The whole framework is developed in a way independent of the underlying logical system (and thus also does not prescribe the nature of the parts of a specification that may be hidden). We also show how various other logic independent specification formalisms can be mapped into development graphs; thus, development graphs can serve as a kernel formalism for management of proofs and of change. 相似文献
15.
作为一种二维的形式化方法,图文法为可视化语言提供了直观而规范的描述手段.然而,大多数图文法形式框架在空间语义处理能力方面有所不足,影响了图文法的表达能力及其实际应用范围.针对现存的问题,构建了一种新型空间图文法形式框架vCGG (virtual-node based coordinate graph grammar).区别于其他空间图文法,vCGG在产生式中通过定义虚结点的概念描述产生式与主图之间的语法结构与空间语义关系,在保留抽象能力的同时,提高了其空间语义配置性能.通过与几种典型空间图文法框架比较,vCGG形式框架在直观性、规范性、表达能力以及分析效率方面均有着较好的表现. 相似文献
16.
Several formalisms to model distributed real-time systems coexist in the literature. This naturally induces a need to compare
their expressiveness and to translate models from one formalism to another when possible. The first formal comparisons of
the expressiveness of these models focused on the preservation of the sequential behavior of the models, using notions like
timed language equivalence or timed bisimilarity. They do not consider preservation of concurrency. In this paper we define
timed traces as a partial order representation of executions of our models for real-time distributed systems. Timed traces
provide an alternative to timed words, and take the distribution of actions into account. We propose a translation between
two popular formalisms that describe timed concurrent systems: 1-bounded time Petri nets (TPN) and networks of timed automata
(NTA). Our translation preserves the distribution of actions, that is we require that if the TPN represents the product of
several components (called processes), then each process should have its counterpart as one timed automaton in the resulting
NTA. 相似文献
17.
The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new
systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct
communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is
a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo
channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been
introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints
imposed by connectors. To ensure that the composed system behaves as intended, we need a wide range of automated verification
tools to assist service composition designers. In this paper, we present our framework for the verification of Reo using the
mCRL2{{\tt mCRL2}} toolset. We unify our previous work on mapping various semantic models for Reo, namely, constraint automata, timed constraint
automata, coloring semantics and the newly developed action constraint automata, to the process algebraic specification language
of mCRL2{{\tt mCRL2}}, address the correctness of this mapping, discuss tool support, and present a detailed example that illustrates the use of
Reo empowered with mCRL2{{\tt mCRL2}} for the analysis of dataflow in service-based process models. 相似文献
18.
Skillicorn D.B. Glasgow J.I. 《IEEE transactions on pattern analysis and machine intelligence》1989,15(2):221-229
A methodology is presented for transforming a functional specification written in Lucid to an equivalent specification that captures its real-time properties. The enhanced specification consists of a set of equations that can be solved for several properties, including execution time and external requirements, or may simply be checked for the existence of a solution. Lucid has a set of meaning-preserving transformations, and a proof system corresponding to a behavioral semantics has been constructed. Both of these tools can be used to reason about properties of the specification. The specification is executable and can be used as a prototype for the system being specified. It is possible to express architectural constraints within the same formal framework. Thus this type of specification can be used to guide the development of new real-time systems 相似文献
19.
20.
混合仿真语言规范不仅要能够定义语言的语法,还要能够定义设计概念的语义规则。本体论能够为描述将语法和语义相结合的语言规范奠定基础。本文基于对混合系统的分析,提出了混合系统高级本体论HyHO,它包括在混合建模和仿真的不同领域都能通用的最基本的规范,主要包括时间、事件、状态等概念及其属性分析。通过HyHO能够研究混合系统的本质属性,确定先进仿真中混合系统的计算模型,以及模型的通用形式化方法,为混合仿真语言规范设计奠定了基础。 相似文献