共查询到9条相似文献,搜索用时 0 毫秒
1.
Richard Bubel Reiner Hähnle 《International Journal on Software Tools for Technology Transfer (STTT)》2005,7(3):197-211
The KeY system allows for the integrated informal and formal development of object-oriented Java software. In this paper we report on a major industrial case study involving safety-critical software for the computation of a particular kind of railway timetable used by train conductors. Our case study includes formal specification of requirements both on the analysis and the implementation level. Particular emphasis in our research is placed on the challenge to make authoring and maintenance of formal specifications easier. We demonstrate that the technique of specification patterns as implemented in KeY for the language OCL yields significant improvements. 相似文献
2.
In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, referred
to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches
based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages
(BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules.
We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive
and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in
pre and post-conditions and to specify them in a regular expression-like notation. The semantics of our extension is formally
defined and provides a foundation for implementing runtime checks. Case studies have been performed to show the effectiveness
our approach. We believe that our approach can be adopted by other BISLs.
相似文献
Ashaveena PerumandlaEmail: |
3.
Automatically Detecting and Visualising Errors in UML Diagrams 总被引:1,自引:0,他引:1
Laura A. Campbell Betty H. C. Cheng William E. McUmber R. E. K. Stirewalt 《Requirements Engineering》2002,7(4):264-287
UML has become the de facto standard for object-oriented modelling. Currently, UML comprises several different notations with no formal semantics attached
to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we developed
a formalisation framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This
paper describes automated structural and behavioural analyses applicable to UML diagrams using our formalisation framework.
In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem
for behavioural analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original
UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modelling
and analysis of UML diagrams for an automotive industrial case study.
Correspondence and offprint requests to: Dr B. Cheng, Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan
State University, 3115 Engineering Building, East Lansing, MI 48824, USA. Tel.: +1 517 355 8344; Fax: +1 517 432 1061; Email:
chengb@cse.msu.edu 相似文献
4.
In this paper, we define a number of tools that we think belong to the core of any toolkit for requirements engineers. The tools are conceptual and hence, they need precise definitions that lay down as exactly as possible what their meaning and possible use is. We argue that this definition can best be achieved by a formal specification of the tool. This means that for each semi-formal requirements engineering tool we should provide a formal specification that precisely specifies its meaning. We argue that this mutually enhances the formal and semi-formal technique: it makes formal techniques more usable and, as we will argue, at the same time simplifies the diagram-based notations.At the same time, we believe that the tools of the requirements engineer should, where possible, resemble the familiar semi-formal specification techniques used in practice today. In order to achieve this, we should search existing requirements specification techniques to look for a common kernel of familiar semi-formal techniques and try to provide a formalisation for these.In this paper we illustrate this approach by a formal analysis of the Shlaer-Mellor method for object-oriented requirements specification. The formal specification language used in this analysis is LCM, a language based on dynamic logic, but similar results would have been achieved by means of another language. We analyse the techniques used in the information model, state model, process model and communication model of the Shlaer-Mellor method, identify ambiguities and redundancies, indicate how these can be eliminated and propose a formalisation of the result. We conclude with a listing of the tools extracted from the Shlaer-Mellor method that we can add to a toolkit that in addition contains LCM as formal specification technique. 相似文献
5.
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. 相似文献
6.
《Expert systems with applications》2014,41(8):3831-3849
Grid computing is the federation of resources from multiple locations to facilitate resource sharing and problem solving over the Internet. The challenge of finding services or resources in Grid environments has recently been the subject of many papers and researches. These researches and papers evaluate their approaches only by simulation and experiments. Therefore, it is possible that some part of the state space of the problem is not analyzed and checked well. To overcome this defect, model checking as an automatic technique for the verification of the systems is a suitable solution. In this paper, an adopted type of resource discovery approach to address multi-attribute and range queries has been presented. Unlike the papers in this scope, this paper decouple resource discovery behavior model to data gathering, discovery and control behavior. Also it facilitates the mapping process between three behaviors by means of the formal verification approach based on Binary Decision Diagram (BDD). The formal approach extracts the expected properties of resource discovery approach from control behavior in the form of CTL and LTL temporal logic formulas, and verifies the properties in data gathering and discovery behaviors comprehensively. Moreover, analyzing and evaluating the logical problems such as soundness, completeness, and consistency of the considered resource discovery approach is provided. To implement the behavior models of resource discovery approach the ArgoUML tool and the NuSMV model checker are employed. The results show that the adopted resource discovery approach can discovers multi-attribute and range queries very fast and detects logical problems such as soundness, completeness, and consistency. 相似文献
7.
The design of a fault-tolerant distributed, real-time, embedded system with safety-critical concerns requires the use of formal
languages. In this paper, we present the foundations of a new software engineering method for real-time systems that enables
the integration of semiformal and formal notations. This new software engineering method is mostly based upon the ”COntinuuM”
co-modeling methodology that we have used to integrate architecture models of real-time systems (Perseil and Pautet in 12th
International conference on engineering of complex computer systems, ICECCS, IEEE Computer Society, Auckland, pp 371–376,
2007) (so we call it “Method C”), and a model-driven development process (ISBN 978-0-387-39361-2 in: From model-driven design
to resource management for distributed embedded systems, Springer, chap. MDE benefits for distributed, real time and embedded
systems, 2006). The method will be tested in the design and development of integrated modular avionics (IMA) frameworks, with
DO178, DO254, DO297, and MILS-CC requirements. 相似文献
8.
Integrating a software architecture-centric method into object-oriented analysis and design 总被引:2,自引:0,他引:2
The choice of methodology for the development of the architecture for software systems has a direct effect on the suitability of that architecture. If the development process is driven by the user’s functional requirements, we would expect the architecture to appropriately reflect those requirements. We would also expect other aspects not captured in the functional specification to be absent from the architecture. The same phenomenon is true in development approaches that stress the importance of systemic quality attributes or other non-functional requirements; those requirements are prominent in the resulting architecture, while other requirement types not stressed by the approach are absent. In other words, the final architecture reflects the focus of the development approach. An ideal approach, therefore, is one that incorporates all goals, expectations, and requirements: both business and technical. To accomplish this we have incorporated, into a single architectural development process, generalized Object-Oriented Analysis and Design (OOAD) methodologies with the software architecture-centric method, the Quality Attribute Workshop (QAW) and Attribute Driven Design (ADD). OOAD, while relatively intuitive, focuses heavily on functional requirements and has the benefit of semantic closeness to the problem domain making it an intuitive process with comprehendible results. Architecture-centric approaches, on the other hand, provide explicit and methodical guidance to an architect in creating systems with desirable qualities and goals. They provide minimal guidance in determining fine-grained architecture, however. The integrated approach described in this paper maximizes the benefits of the respective processes while eliminating their flaws and was applied in a eight university, global development research project with great success. A case study from that experiment is included here to demonstrate the method. 相似文献
9.
Analysis of a biphase mark protocol with Uppaal and PVS 总被引:1,自引:1,他引:0
The biphase mark protocol is a convention for representing both a string of bits and clock edges in a square wave. The protocol is frequently used for communication at the physical level of the ISO/OSI hierarchy, and is implemented on microcontrollers such as the Intel 82530 Serial Communications Controller. An important property of the protocol is that bit strings of arbitrary length can be transmitted reliably, despite differences in the clock rates of sender and receiver (drift), variations of the clock rates (jitter), and distortion of the signal after generation of an edge. In this article, we show how the protocol can be modelled naturally in terms of timed automata. We use the model checker Uppaal to derive the maximal tolerances on the clock rates, for different instances of the protocol, and to support the general parametric verification that we formalized using the proof assistant PVS. Based on the derived parameter constraints we propose instances of BMP that are correct (at least in our model) but have a faster bit rate than the instances that are commonly implemented in hardware.F.W. Vaandrager was supported by EU IST project IST-2001-35304 Advanced Methods for Timed Systems (AMETIST).lA.L. de Groot was supported by NWO project 612.062.000 Architecture for Structuring the requirements Specification of Embedded Safety-critical Systems (ASSESS). 相似文献