Research On Formal Methods For Safe Software Architecture

The research in the field of component-based software architecture plays an increasingly important role in software engineering area. The architecture derived from the components and their assembly can provide rich information for design because it describes both the interactions among modules and the constraints on them. It makes use of some predefined computing models to analyze the intuitive quality of each computing modules and then produces the further analysis of the overall architectural properties. Software architecture reflects the critical properties such as safety under some given configuration desired by the system, thus the decision is made for the design and construct at the early stage. In recent years many ADLs (architectural describing languages) and supporting kits and attributes models for architectural styles have come into being one by one. It enables the possibility of time- and labor-saving analysis of system properties on architectural level and the early error- checking that provides a formal architectural description for a complex software system.At the same time, more and more research is focusing on the safety of software—a new topic in information community. It is a challenging work to make it clear that how to describe, analyze and verify such a non-functional property as safety in software architecture. As one of the quality attributes, the safety ensures that the series of activities can be carried out smoothly in the life cycle of the software development. The target is to eliminate the potential hazard. A precise formal verification or contrary examples can be given on the base of formal description. Formal architectural models include operation-, process algebra-, logic- and net-based ones. However current software tools are mainly restricted original systems and show various limitations on application, the features of description on data structure and its behavior require the process algebra as the main method to verify the security properties. There is considerately lack of the formal research on software architecture, especially on the combination of safety and software architecture. The consistency and complement of component- based architectural development are assumed and maintained through describing, analyzing and verifying the safety of software architecture within a formal framework. So it is of great importance and valuable for practical applications to explore the formal methods on safety of the components and their architecture.In response to the safety problems in software architecture, our main contribution lies in the following:This paper advances systematic research on the model- describing and analyzing, verifying methods for software architectures on various viewpoints;This paper provides a formal framework on the safe software architectures and formally clarifies the conception of safe software architecture;This paper integrates the related theories and approaches about the safe properties of models especially in formal methods;This paper introduces the process algebra language with its powerful standard model-checking tools for safe software architectures and applies them successfully into practice. On the basis of analysis of the existing formal methods and technologies, this paper proposes a formal framework for the safe software architecture in the first part. The necessity of establishing architectural models using components-based software architecture for constructing software systems is explained. The nature of the establishment is to achieve formal models through formal methods in order to describe and verify complex systems. The rigorous mathematical basis of the formal methods guarantees systems confidence and correctness. The system description is based on the architectural models, structural grammars and semantics of the construct, operation and behaviors.Then we discuss how to model behavior, static structure, function, and process of the system. In details we introduce how to describe the behavioral models of safe architecture using states transition system that consists of the notation, modeling steps, etc. The system's Kripke structure is established after the series definitions of stable states, stable sates transitions, reachable transitions, and system behavioral trees. We achieve the safety of the architectural model by verifying the existence of the fixed point on the predicate transformer in the states transition system. Because of the capabilities of describing the parallel behaviors of components, its rigorous algebra nature and its powerful standard equivalences tools, so this paper focuses on process algebra to carry out the research on safety of component-based software architecture. We describe the structure and process models using process-algebra-based language (including its syntax and operational semantics), and then provide the description specification (textual and graphical) on the model. From the definition of the constraint semantics of the component types, architecture types, and components instances, we achieve the semantic of the interactive behaviors arising from the static operator. To be supplement, the static structure model mainly provides architectural definition on the viewpoint of grammar. The functional model combining the operating logic and other formal approaches makes use of temporal logic to describe the system's safety. Additionally, the abilities of the used describing language UML and Wright are analyzed and compared with other languages based on the process algebra.In this paper, we concentrate on a process algebra-based architectural description language, which deals with incompatibility between two components due to a single interaction or the combination of several interactions and with the lack of interoperability among a set of components through architectural compatibility check and interoperability check relying on standard observational equivalences. The adequacy of the architectural compatibility check is assessed on a compressing proxy system, while the adequacy of the architectural interoperability check is assessed on a cruise control system. We then address the issue of scaling the checks to architectural styles though extension of the language, and we show that all the architectures conforming to the same architectural types possess the same compatibility and interoperability properties. This method has the nature of behavior and algebra, by which an architectural description is made up of only the types of components and connectors and the constraint on the topology. Thus a uniform framework is provided for the compositional, hierarchical, graphical architectural description language based on the component-based software architectural specification and analysis. It can ensure the safety within a given set of components interacting with a certain safe component. The architectural model established by such method owns the safety by both checks that turn out to be more convenient for efficiency and/or diagnosis-related reasons than directly verifying safety for the considered set of software components. As a complement of the process algebra-based language, we introduce another architectural safety model aiming at simple communication between two safe components, whose analysis of safety is based on the belief logic. It provides both normal and abnormal interaction protocols between safe components, including the protocol description, analysis and verification. The communicating model is built up taking the safe information fluent through safe components and safe connectors for example. We verify that each time the implement of the model is well remained safe in the existing safe architectural model.The application part is hierarchically carried out in the project of security control personal computer system. Safe software architectural model is made up of software architectural model, the security control operating system model, and the safe access control model, three levels in all. Based on the given security standard, the analysis for the mathematical features of such models as mandatory access control and role-based access control enables the strong basis of the enhanced new model. The establishment of the safe operating system model is completed during the course of the reduce flow graph of the access control architecture, the architectural checks into the original system and the improvement of redefined safe components. The whole procedure shows that the true reason leading to danger is the incorrect division of components and the possible interactions that don't conform the interoperability. Safe operating system on base of the original Linux system uses such improved approaches as information completeness protection, newly adding safe tag. Its realization relies on the safe call of the safe access control mechanism. The overall architectural structure graph of the enhanced security operating system illustrates that the system conforms the Flask structure completely. Additionally as a sample, the LOGIN process illustrates the effective realization of the safe technologies. Finally we introduce the application and expansion of the safe method. We combine the safe architectural models and methods and the software reuse technique. They are safe reuse technologies of the components, software architecture, and the definition of the methods and its practice. The method is also expanded to such other safety-related nonfunctional attributes as interoperability, privacy and the atomic properties.Finally, we summarize what we have achieved and discuss our future work.