Formal Methods for Specifying and Analyzing Complex Software Systems

Formal Methods for Specifying and Analyzing Complex Software Systems

Xudong He (Florida International University, USA), Huiqun Yu (East China University of Science and Technology, China) and Yi Deng (Florida International University, USA)
Copyright: © 2007 |Pages: 27
DOI: 10.4018/978-1-59140-941-1.ch013
OnDemand PDF Download:


Software has been a major enabling technology for advancing modern society, and is now an indispensable part of daily life. Because of the increased complexity of these software systems, and their critical societal role, more effective software development and analysis technologies are needed. How to develop and ensure the dependability of these complex software systems is a grand challenge. It is well known that a highly dependable complex software system cannot be developed without a rigorous development process and a precise specification and design documentation. Formal methods are one of the most promising technologies for precisely specifying, modeling, and analyzing complex software systems. Although past research experience and practice in computer science have convincingly shown that it is not possible to formally verify program behavior and properties at the program source code level due to its extreme huge size and complexity, recently advances in applying formal methods during software specification and design, especially at software architecture level, have demonstrated significant benefits of using formal methods. In this chapter, we will review several well-known formal methods for software system specification and analysis. We will present recent advances of using these formal methods for specifying, modeling, and analyzing software architectural design.

Complete Chapter List

Search this Book:
Table of Contents
Du Zhang
Du Zhang
Chapter 1
J. J. Dolado, D. Rodríguez, J. Riquelme, F. Ferrer-Troyano, J. J. Cuadrado
One of the problems found in generic project databases, where the data is collected from different organizations, is the large disparity of its... Sample PDF
A Two-Stage Zone Regression Method for Global Characterization of a Project Database
Chapter 2
Marek Reformat, Petr Musilek, Efe Igbide
Amount of software engineering data gathered by software companies amplifies importance of tools and techniques dedicated to processing and analysis... Sample PDF
Intelligent Analysis of Software Maintenance Data
Chapter 3
Gary D. Boetticher
Given a choice, software project managers frequently prefer traditional methods of making decisions rather than relying on empirical software... Sample PDF
Improving Credibility of Machine Learner Models in Software Engineering
Chapter 4
Daniele Gunetti
Though inductive logic programming (ILP for short) should mean the “induction of logic programs”, most research and applications of this area are... Sample PDF
ILP Applications to Software Engineering
Chapter 5
Min Chen, Shu-Ching Chen
This chapter introduces an advanced content-based image retrieval (CBIR) system, MMIR, where Markov model mediator (MMM) and multiple instance... Sample PDF
MMIR: An Advanced Content-Based Image Retrieval System Using a Hierarchical Learning Framework
Chapter 6
I-Ling Yen, Tong Gao
Reconfigurability is an important requirement in many application systems. Many approaches have been proposed to achieve static/dynamic... Sample PDF
A Genetic Algorithm-Based QoS Analysis Tool for Reconfigurable Service-Oriented Systems
Chapter 7
Witold Pedrycz, Giancarlo Succi
The learning abilities and high transparency are the two important and highly desirable features of any model of software quality. The transparency... Sample PDF
Fuzzy Logic Classifiers and Models in Quantitative Software Engineering
Chapter 8
Jelber Sayyad Shirabad, Timothy C. Lethbridge, Stan Matwin
This chapter presents the notion of relevance relations, an abstraction to represent relationships between software entities. Relevance relations... Sample PDF
Modeling Relevance Relations Using Machine Learning Techniques
Chapter 9
Yi Liu, Taghi M. Khoshgoftaar
A software quality estimation model is an important tool for a given software quality assurance initiative. Software quality classification models... Sample PDF
A Practical Software Quality Classification Model Using Genetic Programming
Chapter 10
Yan Ma, Lan Guo, Bojan Cukic
Accurate prediction of fault-prone modules in software development process enables effective discovery and identification of the defects. Such... Sample PDF
A Statistical Framework for the Prediction of Fault-Proneness
Chapter 11
Bhekisipho Twala, Michelle Cartwright, Martin Shepperd
Recently, the use of machine learning (ML) algorithms has proven to be of great practical value in solving a variety of software engineering... Sample PDF
Applying Rule Induction in Software Prediction
Chapter 12
Baowen Xu, Xiaoyuan Xie, Liang Shi, Changhai Nie
Genetic algorithms are a kind of global meta-heuristic search technique that searches intelligently for optimal solutions to a problem. Evolutionary... Sample PDF
Application of Genetic Algorithms in Software Testing
Chapter 13
Xudong He, Huiqun Yu, Yi Deng
Software has been a major enabling technology for advancing modern society, and is now an indispensable part of daily life. Because of the increased... Sample PDF
Formal Methods for Specifying and Analyzing Complex Software Systems
Chapter 14
Paul Dietz, Aswin van den Berg, Kevin Marth, Thomas Weigert, Frank Weil
Model-driven engineering proposes to develop software systems by first creating an executable model of the system design and then transforming this... Sample PDF
Practical Considerations in Automatic Code Generation
Chapter 15
Donghua Deng, Phillip C.Y. Sheu
This chapter presents a distributed proactive semantic software engineering environment (DPSSEE) that incorporates logic rules into a software... Sample PDF
DPSSEE: A Distributed Proactive Semantic Software Engineering Environment
Chapter 16
Shangping Ren, Jeffrey J.P. Tsai, Ophir Frieder
In this chapter, we present the role-based context constrained access control (RBCC) model. The model integrates contextual constraints specified in... Sample PDF
Adding Context into an Access Control Model for Computer Security Policy
About the Editors
About the Authors