Skip to main content

2010 | Buch

Verification and Validation in Systems Engineering

Assessing UML/SysML Design Models

verfasst von: Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh

Verlag: Springer Berlin Heidelberg

insite
SUCHEN

Über dieses Buch

At the dawn of the 21st century and the information age, communication and c- puting power are becoming ever increasingly available, virtually pervading almost every aspect of modern socio-economical interactions. Consequently, the potential for realizing a signi?cantly greater number of technology-mediated activities has emerged. Indeed, many of our modern activity ?elds are heavily dependant upon various underlying systems and software-intensive platforms. Such technologies are commonly used in everyday activities such as commuting, traf?c control and m- agement, mobile computing, navigation, mobile communication. Thus, the correct function of the forenamed computing systems becomes a major concern. This is all the more important since, in spite of the numerous updates, patches and ?rmware revisions being constantly issued, newly discovered logical bugs in a wide range of modern software platforms (e. g. , operating systems) and software-intensive systems (e. g. , embedded systems) are just as frequently being reported. In addition, many of today’s products and services are presently being deployed in a highly competitive environment wherein a product or service is succeeding in most of the cases thanks to its quality to price ratio for a given set of features. Accordingly, a number of critical aspects have to be considered, such as the ab- ity to pack as many features as needed in a given product or service while c- currently maintaining high quality, reasonable price, and short time -to- market.

Inhaltsverzeichnis

Frontmatter
Chapter 1. Introduction
Abstract
In this day and age, various forms of programming and computation are commonplace in our immediate urban surroundings, often embedded in sensors, traffic and other driving-related assistance, public advertisements, hotspots, smart elevators, and many other micro-controller or CPU-based systems. Moreover, wearable electronics, like mobile phones, PDAs, and the likes, are more popular than ever. Thus, in modern engineering fields, especially those related to software-intensive systems, the solution space available to the designers and engineers is significantly increased due to the presence of the programmable aspect.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 2. Architecture Frameworks, Model-Driven Architecture, and Simulation
Abstract
With the introduction and rapid success of the personal computer (PC) in the late 1970s, numerous computer applications were marketed to support the users in various domains. In the SE domain particularly, along with these software applications, several languages both formal and informal like VHDL [246], Petri Net family [4], IDEF [154, 242], UML [184], and SysML [255] were created to support developers in capturing essential aspects of the systems being engineered. The system properties usually reflect structural, temporal, or functional aspects and could be related to various areas such as processes, information infrastructures, internal systems/components, interoperability with other systems, and user interactions.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 3. Unified Modeling Language
Abstract
The unified modeling language (UML) [185, 186] is a standardized general-purpose modeling language that lets one to specify, visualize, build, and document the artifacts of software-intensive systems. The goal of such a language is to model software systems prior to construction and concurrently automates the production, improves the quality, reduces the inferred costs, and shortens time to market. The resulting models represent systems at different levels of detail prior to their actual implementation.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 4. Systems Modeling Language
Abstract
Systems modeling language (SysML) [187] is a modeling language dedicated to systems engineering applications. It is a UML profile that not only reuses a subset of UML 2.1.1 [186] but also provides additional extensions to better fit SE’s specific needs. These extensions are mainly meant to address the requirements stated in the UML for SE request for proposal (RFP) [177]. It is intended to help specify and architect complex systems and their components and enable their analysis, design, and verification and validation. These systems may consist of heterogeneous components such as hardware, software, information, processes, personnel, and facilities [187].
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 5. Verification, Validation, and Accreditation
Abstract
There exist many definitions for the terms verification and validation, depending on the group concerned or the domain of application. In the SE world, the most widely used definitions of these terms are provided by the Defense Modeling and Simulation Organization (DMSO) [67, 168]. On the one hand, verification is defined as “the process of determining that a model implementation and its associated data accurately represent the developer’s conceptual description and specifications” [67]. On the other hand, validation is defined as “the process of determining the degree to which a model and its associated data provide an accurate representation of the real world from the perspective of the model’s intended use” [67].
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 6. Automatic Approach for Synergistic Verification and Validation
Abstract
Modeling languages, such as UML 2.x and SysML, support model-based systems engineering. They are commonly used to specify, visualize, store, document, and exchange design models. Generally, they contain all the syntactic, semantic, and presentation information regarding a given application domain. A model is a representation of the system that is used to compile the requirements in order to create executable specifications. These specifications model the system at a high level of abstraction and include all the information needed to specify the software or hardware implementation. Specific diagrams are used to capture some of the system’s important aspects:
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 7. Software Engineering Metrics in the Context of Systems Engineering
Abstract
The need for reliable and high-performing software led to the emergence of software engineering. Since the birth of software engineering in 1968, new approaches and techniques were developed to govern the quality of software systems. Software metrics are used to assess the quality of software systems in terms of system attributes such as complexity, understandability, maintainability, stability. Different software metrics have been developed to measure the quality of structural and objected-oriented programming techniques.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 8. Verification and Validation of UML Behavioral Diagrams
Abstract
It is generally accepted that any system that has an associated dynamics can be abstracted to one that evolves within a discrete state space. Such a system is able to evolve through its state space assuming different configurations, where a configuration can be understood as the set of states to which the system abides at any particular moment. Hence, all the possible configurations summed up by the dynamics of the system, and the transitions thereof, can be coalesced into a configuration transition system (CTS).
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 9. Probabilistic Model Checking of SysML Activity Diagrams
Abstract
Incorporated modeling and analysis of both functional and non-functional aspects of today’s systems behavior represents a challenging issue in the field of formal methods.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 10. Performance Analysis of Time-Constrained SysML Activity Diagrams
Abstract
Many modern systems are now being developed by aggregating other subsystems and components that may have different expected, though not exactly determined, characteristics and features. As such, these kinds of systems may exhibit features such as concurrency and probabilistic behavior. In this context, appropriate models are needed in order to effectively capture the system behavior.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 11. Semantic Foundations of SysML Activity Diagrams
Abstract
In this chapter, we propose to study the semantic foundations of SysML activity diagrams. A formalization of the semantics will allow us to build a sound and rigorous framework for the V&V of design models expressed using these diagrams. To this end, we design a dedicated formal language, called activity calculus (AC), used in order to mathematically express and analyze the behaviors captured by SysML activity diagrams.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 12. Soundness of the Translation Algorithm
Abstract
In this chapter, our main objective is to closely examine the correctness of the translation procedure proposed earlier that maps SysML activity diagrams into the input language of the probabilistic model checker PRISM. In order to provide a systematic proof, we rely on formal methods, which enable us with solid mathematical basis. To do so, four main ingredients are needed. First, we need to express formally the translation algorithm. This enables its manipulation forward deriving the corresponding proofs. Second, the formal syntax and semantics for SysML activity diagrams need to be defined. This has been proposed in the previous chapter by the means of the activity calculus language. Third, the formal syntax and semantics of PRISM input language have to be defined. Finally, a suitable relation is needed in order to compare the semantics of the diagram with the semantics of the resulting PRISM model.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Chapter 13. Conclusion
Abstract
Many mature technologies,1 accompanied by ever improving and automated processes of production, brought about an increasing availability of different specialized systems and sub-systems that provide specific functionalities, such as wired and wireless data link connectivity, data storage, analog/digital signal processing, encryption. In addition, in order to benefit from hardware and software reuse, the specialization of such systems is often achieved with corresponding control software along with various libraries or APIs. In fact, today’s software aspect is so pervasive that even systems that have been traditionally mechanical in nature, such as automobiles, are integrating more and more control software to optimize such things as fuel consumption, cruise control, or sensor data processing.
Mourad Debbabi, Fawzi Hassaïne, Yosr Jarraya, Andrei Soeanu, Luay Alawneh
Backmatter
Metadaten
Titel
Verification and Validation in Systems Engineering
verfasst von
Mourad Debbabi
Fawzi Hassaïne
Yosr Jarraya
Andrei Soeanu
Luay Alawneh
Copyright-Jahr
2010
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-15228-3
Print ISBN
978-3-642-15227-6
DOI
https://doi.org/10.1007/978-3-642-15228-3

Premium Partner