共查询到10条相似文献,搜索用时 156 毫秒
1.
Thomas Hildebrandt Raghava Rao Mukkamala Tijs Slaats Francesco Zanitti 《The Journal of Logic and Algebraic Programming》2013,82(5-7):164-185
We conservatively extend the declarative Dynamic Condition Response (DCR) Graph process model, introduced in the PhD thesis of the second author, to allow for discrete time deadlines. We prove that safety and liveness properties can be verified by mapping finite timed DCR Graphs to finite state transition systems. We exemplify how deadlines can introduce time-locks and deadlocks and violate liveness. We then prove that the general technique for safe distribution of DCR Graphs provided in previous work can be extended to timed DCR Graphs. We exemplify the use of timed DCR Graphs and the distribution technique in praxis on a timed extension of a cross-organizational case management process arising from a previous case study. The example shows how a timed DCR Graph can be used to describe the global contract for a timed workflow process involving several organizations, which can then be distributed as a network of communicating timed DCR Graphs describing the local contract for each organization. 相似文献
2.
Christo Angelov Wei Guan Nicolae Marian Feng Zhou Krzysztof Sierszecki S?ren Top 《Innovations in Systems and Software Engineering》2012,8(1):79-92
The widespread use of embedded systems requires the creation of industrial software technology that will make it possible
to engineer systems being correct by construction. That can be achieved through the use of validated (trusted) components,
verification of design models, and automatic configuration of applications from validated design models and trusted components.
This design philosophy has been instrumental for developing COMDES—a component-based framework for distributed embedded control
systems. A COMDES application is conceived as a network of embedded actors that are configured from instances of reusable,
executable components—function blocks (FBs). System actors operate in accordance with a timed multitasking model of computation,
whereby I/O signals are exchanged with the controlled plant at precisely specified time instants, resulting in the elimination
of I/O jitter. The paper presents an analysis technique that can be used to validate COMDES design models in SIMULINK. It
is based on a transformation of the COMDES design model into a SIMULINK analysis model, which preserves the functional and
timing behaviour of the application. This technique has been employed to develop a feasible (light-weight) analysis method
based on runtime observers. The latter are conceived as special-purpose actors running in parallel with the application actors,
while checking system properties specified in Linear Temporal Logic. Observers are configured from reusable FBs that can be
exported to SIMULINK in the same way as application components, making it possible to analyze system properties via simulation.
The discussion is illustrated with an industrial case study—a Medical Ventilator Control System, which has been used to validate
the developed design and analysis methods. 相似文献
3.
This article discusses a new format of predicate diagrams for the verification of real-time systems. We consider systems that
are defined as extended timed graphs, a format that combines timed automata and constructs for modelling data, possibly over
infinite domains. Predicate diagrams are succinct and intuitive representations of Boolean abstractions. They also represent
an interface between deductive tools used to establish the correctness of an abstraction, and model checking tools that can
verify behavioral properties of finite-state models. The contribution of this article is to extend the format of predicate
diagrams to timed systems. We establish a set of verification conditions that are sufficient to prove that a given predicate
diagram is a correct abstraction of an extended timed graph; these verification conditions can often be discharged with SMT
solvers such as CVC-lite. Additionally, we describe how this approach extends naturally to the verification of parameterized
systems. The formalism is supported by a toolkit, and we demonstrate its use at the hand of Fischer’s real-time mutual-exclusion
protocol. 相似文献
4.
Component-based software development is a promising approach for controlling the complexity and quality of software systems.
Nevertheless, recent advances in quality control techniques do not seem to keep up with the growing complexity of embedded
software; embedded systems often consist of dozens to hundreds of software/hardware components that exhibit complex interaction
behavior. Unanticipated quality defects in a component can be a major source of system failure. To address this issue, this
paper suggests a design verification approach integrated into the model-driven, component-based development methodology Marmot. The notion of abstract components—the basic building blocks of Marmot—helps to lift the level of abstraction, facilitates high-level reuse, and reduces verification complexity by localizing verification
problems between abstract components before refinement and after refinement. This enables the identification of unanticipated design errors in the early stages of development. This work
introduces the Marmot methodology, presents a design verification approach in Marmot, and demonstrates its application on the development of a μ-controller-based abstraction of a car mirror control system. An application on TinyOS shows that the approach helps to reuse
models as well as their verification results in the development process. 相似文献
5.
Network invariants for real-time systems 总被引:1,自引:0,他引:1
We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems. We introduce timed transition structures (which are similar in spirit to timed automata) and define a notion of abstraction that is safe with respect to linear temporal properties. We strengthen the notion of abstraction to allow a finite system, then called
network invariant, to be an abstraction of networks of real-time systems. In general the problem of checking abstraction of real-time systems
is undecidable. Hence, we provide sufficient criteria, which can be checked automatically, to conclude that one system is
an abstraction of a concrete one. Our method is based on timed superposition and discretization of timed systems. We exemplify our approach by proving mutual exclusion of a simple protocol inspired by Fischer’s protocol,
using the model checker TLV.
Part of this work was done during O. Grinchtein’s stay at Weizmann Institute.
This author was supported by the European Research Training Network “Games”. 相似文献
6.
We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-;time properties of reactive systems. The abstract notion of timed transition systems generalizes traditional transition systems conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. This framework can model real-time systems that communicate either through shared variables or by message passing and real-time issues such as timeouts, process priorities (interrupts), and process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit references to time through a special clock variable. Corresponding to the two styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules for establishing bounded-invariance and bounded-responce properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and response properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties. 相似文献
7.
Mohammad Ashjaei Nima Khalilzad Saad Mubeen Moris Behnam Ingo Sander Luis Almeida Thomas Nolte 《Real-Time Systems》2017,53(6):916-956
Contemporary distributed embedded systems in many domains have become highly complex due to ever-increasing demand on advanced computer controlled functionality. The resource reservation techniques can be effective in lowering the software complexity, ensuring predictability and allowing flexibility during the development and execution of these systems. This paper proposes a novel end-to-end resource reservation model for distributed embedded systems. In order to support the development of predictable systems using the proposed model, the paper provides a method to design resource reservations and an end-to-end timing analysis. The reservation design can be subjected to different optimization criteria with respect to runtime footprint, overhead or performance. The paper also presents and evaluates a case study to show the usability of the proposed model, reservation design method and end-to-end timing analysis. 相似文献
8.
Summary. When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given
at different levels of abstraction. Suggested verification techniques in the literature include refinement mappings and various
forms of simulation. We present a verification method, in which refinement between two systems is proven by constructing a
transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system. The transducer
uses a FIFO queue that holds segments of the concrete computation that have not been matched yet. This allows a finite delay between
the occurrence of a concrete event and the determination of the corresponding abstract event. This delay often makes the use
of prophecy variables or backward simulation unnecessary.
An important generalization of the method is to prove refinement modulo some transformation on the observed sequences of events.
The method is adapted by replacing the FIFO queue by a component that allows the appropriate transformation on sequences of events. A particular case is partial-order refinement, i.e., refinement that preserves only a subset of the orderings between events of a system. Examples are sequential consistency
and serializability. The case of sequential consistency is illustrated on a proof of sequential consistency of a cache protocol. 相似文献
9.
利用形式化方法对复杂实时构件系统的时序行为进行建模与验证对于提高安全攸关实时构件系统的正确性、可靠性与安全性具有重要意义。介绍了基于时间行为协议的构件时序行为的形式化建模和相容性验证方法,给出了时间行为协议建模与相容性验证工具TCBV的系统架构与功能模块。TCBV应用方便,能够实现实时构件时序行为模型的图形化表示,并可对复杂交互行为的相容性进行自动验证。结合应用实例,介绍了如何利用TCBV对复杂实时构件系统的时序行为进行建模和验证。最后,将TCBV与其它相关工具进行了比较。 相似文献
10.
Representing design decisions for complex software systems, tracing them to code, and enforcing them throughout the lifecycle are pressing concerns for software architects and developers. To be of practical use, specification and modeling languages for software design need to combine rigor with abstraction and simplicity, and be supported by automated design verification tools that require minimal human intervention. This paper examines closely the use of the visual language of Codecharts for representing design decisions and demonstrate the process of verifying the conformance of a program to the chart. We explicate the abstract semantics of segments of the Java package java.awt as a finite structures, specify the Composite design pattern as a Codechart and unpack it as a set of formulas, and prove that the structure representing the program satisfies the formulas. We also describe a set of tools for modeling design patterns with Codecharts and for verifying the conformance of native (plain) Java programs to the charts. 相似文献