Contents 1 UML http://www.uml.org/ UML for Java Programmers UML Distill 3ed 2 rCOS and Zhiming Liu Deadlock checking by a behavioral effect system for lock handling Robustness testing for software components rCOS: Theory and Tool for Component-Based Model Driven Development rCOS: a formal model-driven engineering method for component-based software Graph transformations for object-oriented refinement rCOS: Refinement of Component and Object Systems Refinement of Models of Software Components rCos tutorial slide: Unblockable Compositions of Software Components Ensemble Engineering and Emergence 面向服务架构中服务实现的策略 3 Sun Meng （孙猛） Towards the Introduction of QoS Information in a Component Model 4 others 一种基于构件演算的主动构件精化方法 Unifying Theories of Programming 1 UML UML for Java Programmers Robert Cecil Martin Prentice Hall, Englewood Cliffs, New Jersey 2002 UML for Java Programmers.zip UML_for_Java_Programmers.ppt src.zip UML Distill UML Distilled 3 Edition A Brief Guide to the Standard Object Modeling Language Martin Fowler, Kendall Scott Publisher: Addison Wesley Chapter 1. Introduction 1.1 What Is the UML? The Unified Modeling Language (UML) 1.2 Ways of Using the UML 1.3 How We Got to the UML 1.4 Notations and Meta-Models 1.5 UML Diagrams UML 2 describes 13 official diagram types listed in Table 1.1 and classified as indicated on Figure 1.2. 1.6 What Is Legal UML? 1.7 The Meaning of UML Chapter 2. Development Process 2.1 Iterative and Waterfall Processes 2.2 Predictive and Adaptive Planning 2.3 Agile Processes 2.4 Rational Unified Process All RUP projects should follow four phases. 2.5 Fitting a Process to a Project 2.6 Fitting the UML into a Process 2.6.1 Requirements Analysis 2.6.2 Design 2.6.3 Documentation 2.7 Choosing a Development Process Chapter 3. Class Diagrams: The Essentials 3.1 Properties two quite distinct notations: attributes and associations. 3.1.1 Attributes 3.1.2 Associations 3.2 When to Use Class Diagrams a few tips: structure vs. behavior 3.3 Where to Find Out More 3.4 Multiplicity 3.5 Programming Interpretation of Properties 3.6 Bidirectional Associations 3.7 Operations query vs. modifiers 3.8 Generalization inheritance 3.9 Notes and Comments 3.10 Dependency 3.11 Constraint Rules Object Constraint Language (OCL) Chapter 4. Sequence Diagrams Interaction diagrams: describe how groups of objects collaborate in some behavior. 4.1 Creating and Deleting Participants 4.2 Loops, Conditionals, and the Like 4.3 Synchronous and Asynchronous Calls 4.4 When to Use Sequence Diagrams Chapter 5. Class Diagrams: Advanced Concepts 5.1 Keywords A profile 5.2 Classification and Generalization 5.3 Multiple and Dynamic Classification 5.4 Association Class 5.5 Template (Parameterized) Class 5.6 Enumerations 5.7 Active Class 5.8 Visibility 5.9 Message 5.10 Responsibilities 5.11 Static Operations and Attributes 5.12 Aggregation and Composition 5.13 Derived Properties 5.14 Interfaces and Abstract Classes 5.15 Read-Only and Frozen 5.17 Reference Objects and Value Objects 5.18 Qualified Associations Chapter 6. Object Diagrams Chapter 7. Package Diagrams Chapter 8. Deployment Diagrams Chapter 9. Use Cases A scenario: a sequence of steps describing an interaction between a user and a system A use case: a set of scenarios tied together by a common user goal An actor: a role that a user plays with respect to the system 9.1 Content of a Use Case 9.2 Use Case Diagrams The use case diagram shows the actors, the use cases, and the relationships between them: ·- Which actors carry out which use cases ·- Which use cases include other use cases 9.3 Levels of Use Cases 9.4 Use Cases and Features (or Stories) 9.5 When to Use Use Cases Chapter 10. State Machine Diagrams 10.1 Internal Activities 10.2 Activity States 10.3 Superstates 10.4 Concurrent States 10.5 Implementing State Diagrams 10.6 When to Use State Diagrams Chapter 11. Activity Diagrams Activity diagrams are a technique to describe procedural logic, business process, and work flow 11.1 Decomposing an Action 11.2 And There's More 11.3 When to Use Activity Diagrams 11.4 Where to Find Out More Petri nets 11.5 Partitions 11.6 Signals 11.7 Tokens 11.8 Flows and Edges 11.9 Pins and Transformations 11.10 Expansion Regions 11.11 Flow Final 11.12 Join Specifications Chapter 12. Communication Diagrams Chapter 13. Composite Structures Chapter 14. Component Diagrams Chapter 15. Collaborations Chapter 16. Interaction Overview Diagrams Chapter 17. Timing Diagrams UML Distilled, 3rd Ed (Martin Fowler - Addison Wesley).pdf rCOS Deadlock checking by a behavioral effect system for lock handling Ka I Pun, Martin Steffen, Volker Stolza The Journal of Logic and Algebraic Programming 81 (2012) 331–354 Abstract: Deadlocks are a common error in programs with lock-based concurrency and are hard to avoid or even to detect. Oneway for deadlock prevention is to statically analyze the program code to spot sources of potential deadlocks. Often static approaches try to confirm that the lock-taking adheres to a given order, or, better, to infer that such an order exists. Such an order precludes situations of cyclic waiting for each other’s resources, which constitute a deadlock. In contrast, we do not enforce or infer an explicit order on locks. Instead we use a behavioral type and effect system that, in a first stage, checks the behavior of each thread or process against the declared behavior, which captures potential interaction of the thread with the locks. In a second step on a global level, the state space of the behavior is explored to detect potential deadlocks.We define a notion of deadlock-sensitive simulation to prove the soundness of the abstraction inherent in the behavioral description. Soundness of the effect system is proven by subject reduction, formulated such that it captures deadlock-sensitive simulation. To render the state-space finite,we show two further abstractions of the behavior sound, namely restricting the upper bound on re-entrant lock counters, and similarly by abstracting the (in general context-free) behavioral effect into a coarser, tail-recursive description. We prove our analysis sound using a simple, concurrent calculus with re-entrant locks. Keywords: Concurrency, Deadlock prevention, Static analysis, Behavioral type and effect systems, Simulation relation, Abstraction Deadlock Checking by a Behavioral Effect System for Lock Handling.pdf Robustness testing for software components Bin Lei, Xuandong Li, Zhiming Liu, Charles Morisset, Volker Stolz Science of Computer Programming 75 (2010) 879-897 Abstract: Component-based development allows one to build software from existing components and promises to improve software reuse and reduce costs. For critical applications, the user of a component must ensure that it fits the requirements of the application. To achieve this, testing is a well-suited means when the source code of the components is not available. Robustness testing is a testing methodology to detect the vulnerabilities of a component under unexpected inputs or in a stressful environment. As components may fail differently in different states, we use a state machine based approach to robustness testing. First, a set of paths is generated to cover transitions of the state machine, and it is used by the test cases to bring the component into a specific control state. Second, method calls with invalid inputs are fed to the component in different states to test the robustness. By traversing the paths, the test cases cover more states and transitions compared to stateless API testing.We apply our approach to several components, including open source software, and compare our results with existing approaches. 1. Introduction Component based design: how to use existing components in the design or maintenance of a new and larger application. three major properties: -- the fitness -- the correctness -- the robustness, rCOS: theory of component-based design The objective of the work: to present generate test cases to detect robustness failures the organization of this paper: 1) section 2 introduces the rCOS method for component based design, focusing on the notion of contracts and implementation of components, and defining what we mean when we say an implementation is correct. 2) Section 3 defines robust components and discuss the causes of non-robustness so as to motivate our method. 3) Section 4 describes the methodology of the protocol based testing framework. 4) Section 5 outline the implementation of the prototype tool and give experimental results for the evaluation of our tool. 5) Section 6 discuss related work, summarise our work, and give a plan of future work 2. Component contracts 2.1. UTP as root of semantic theory unifying theories 2.2. Interfaces and their contracts main concepts in rCos -- Interfaces. -- Contracts 2.3. Component implementation 3. Robustness testing 3.1. Causes of robustness failures -- an incomplete contract specification 3.2. Robustness test case 3.3. Exceptions and robustness 4. Method 4.1. Path generation 4.2. Parameter generation for object oriented programs 4.3. Analysis of preconditions 5. Tool implementation and experimental results 6. Related work and conclusions 6.1. Related work 6.2. Conclusions 6.3. Future work Robustness Testing for Software Components.pdf rCOS: Theory and Tool for Component-Based Model Driven Development Zhiming Liu, Charles Morisset, and Volker Stolz FSEN 2009, LNCS 5961, pp. 62–80, 2010 Abstract. We present the roadmap of the development of the rCOS theory and its tool support for component-based model driven software development (CB-MDD). First the motivation for using CB-MDD, its needs for a theoretical foundation and tool support are discussed, followed by a discussion of the concepts, techniques and design decisions in the research of the theory and the development of the prototype tool. The concepts, techniques and decisions discussed here have been formalized and published. References to those publications are provided with explanations. Based on the initial experiences with a case study and the preliminary rCOS tool development, further development trajectory leading to further integration with transformation and analysis plug-ins is delineated. Keywords: contract, component, design pattern, model transformation. 1 Introduction four fundamental attributes： -- the complexity of the domain application, -- the difficulty of managingthe development process, -- the flexibility possible to offer through software, -- the problem of characterizing the behavior of software systems interoperability： the aim of this paper: to present the rCOS approach to CB-MDD for handling software complexity. the organization of this paper: 1) Section 2 motivates the research in the rCOS modeling theory and the development of a prototype tool. -- first show how CB-MDD is a natural path in the advance of software engineering in handling complexity by separation of concerns. -- then followed by a discussion of the key theme, principles,challenges, and essential techniques of a component-based model driven approach. 2) Section 3 summarize the theoretical aspects of rCOS and show how they meet the needs discussed in Sect.2 3) Section 4 reports our initial experience with the tool, and based on the lessons learned, we delineate the further development trajectory leading to further integration with transformation and analysis plug-ins. 4) Section 5 gives concluding remarks 2 Natural Path to CB-MDD the complexity of a system - separation of concerns waterfall model：requirements capture and analysis, design, coding and testing 2.1 Early Notions of Components and Models modules - component the principles: -- structured programming -- modularization the spiral model: -- project management --risks control software defect detection: - tools two different models:state based, event based and property based 2.2 Theoretical and Tool Support to Successful CB-MDD The discipline: – each phase is based on the construction of models, – models in later phases are constructed from those in earlier phases by model transformations, – code is an executable model generated from models in the design phase. For a safety critical application: – the models constructed are verifiable, – model transformation are proven to preserve desirable properties of the models, such as functional correctness, and – the model transformations generate conditions about the models, called proof obligations, that are verified by using verification techniques and tools. component-based model driven design: -- theoretical foundation -- strong technical and tool support the key features of this modeling approach: -- Multi-dimensional separation of concerns. -- Object-orientation in CB-MDD. -- Component-based architecture. -- Scaling and automating refinement. -- data functionality refinement -- interaction refinement --object-oriented structure refinement -- Tool supported development process. 3 Theoretical Foundation of rCOS 3.1 Component Implementation and Component Refinement -- Interfaces: -- UTP as root of semantic theory. -- Semantics and refinement of components. -- Object-orientation in rCOS. 3.2 Contracts requirements analysis model - a design model - an implementation model. actor: -- Contracts for black-box modeling. -- Refinement of contracts. -- Correctness of components. -- Component publications and their faithfulness. -- Theorem of separation of concerns. contracts +publications of an interface -a notion of extended contract a contract: a black box behavior model of interfaces 3.3 Publications 3.4 Composition components coordination: Internalization and plugging -- Composition of contracts and publications of components -- Composition of component implementations. -- Compositional modeling, refinement and verification. 4 The rCOS Tool a UML profile -rCOS 4.1 Tool Support to Requirement Analysis 4.2 Model Transformation Tool to Support Design threes kinds of model transformations: -- Object-oriented design of a component. -- 5 Concluding Remarks the purpose of this paper: presented the motivation, the theme, the features and challenges of the rCOS theory and its tool support themain challenge: rCOS theory and tools for component-based model driven development.pdf rCOS: a formal model-driven engineering method for component-based software Wei KE, Xiaoshan L, Zhiming LIU, Volker STOLZ Front. Comput. Sci., 2012, 6(1): 17–39 Abstract Model-driven architecture (MDA) has become a main stream technology for software-intensive system design. The main engineering principle behind it is that the inherent complexity of software development can only be mastered by building, analyzing and manipulating system models. MDA also deals with system complexity by providing component-based design techniques, allowing independent component design, implementation and deployment, and then system integration and reconfiguration based on component interfaces. The model of a system in any stage is an integration of models of different viewpoints. Therefore, for a model-driven method to be applied effectively, it must provide a body of techniques and an integrated suite of tools for model construction, validation, and transformation. This requires a number of modeling notations for the specification of different concerns and viewpoints of the system. These notations should have formally defined syntaxes and a unified theory of semantics. The underlying theory of the method is needed to underpin the development of tools and correct use of tools in software development, as well as to formally verify and reason about properties of systems in mission-critical applications. The modeling notations, techniques, and tools must be designed so that they can be used seamlessly in supporting development activities and documentation of artifacts in software design processes. This article presents such a method, called the rCOS, focusing on the models of a system at different stages in a software development process, their semantic integration, and how they are constructed, analyzed, transformed, validated, and verified. Keywords component-based design, models, model transformations, verification, tool support 1 Introduction The root of “software crisis: the inherent complexity of software 1.1 Software complexity the characterisitics of software complexity: -- the complexity of the domain application -- the difficulty of managing the development process -- the flexibility possible to offer through software -- the problem of characterizing the behavior of software systems software-intensive systems: new features of software: distributed, dynamic, and mobile 1.2 Formal model-driven development model-driven architecture (MDA) Key features of MDA: -- abstraction for information hiding in order to focus on a concern at a time -- decomposition to divide and conquer -- incremental development so as to allow the use of different techniques and tools. main problems of MDA: lacks systematic techniques and tool support 1.3 The aim and theme of rCOS The aim of the rCOS project: to research, develop, and teach a method and its tools for predictable development of reliable software. 1.4 Organization 1) Section 2 present the rCOS approach to handling software complexity, thus motivating the different models in rCOS. 2) Section 3 discuss the semantic foundation of these models and point the reader to the literature on the relevant theories and techniques. 3) Section 4 defines the models of components, their refinement relations and compositions. 4) Section 5 discusses how the different models are built and validated in a development process. 5) Section 6 gives concluding remarks and future work. 2 Mastering complexity with rCOS the goal of this section: the main ideas behind the development of the rCOS method that aim at mastering software complexity by separation of concerns, decomposition, and rigorous use of abstraction. 2.1 rCOS support to model-driven development the principles of model-driven development and formal methods: • Abstraction • Decomposition • Separation of concerns • Model transformations • Use of formalization 2.2 rCOS support to component-based development the contracts of the interfaces of components rCOSP: a componentbased architecture definition language of rCOS 2.3 The format of component specifications in rCOSP rCOSP proposes a Java-stylespecification language The format of a component specification in rCOSP is shown in Fig. 3 • Interfaces of components • Data functionality • Actions • Interaction protocols • Class structure and data types Example 1 Fig. 4 shows the architecture 3 Unifying theories for component-based software modeling the separation of concerns a) control the complexity of the models b) allow the use of different techniques and tools of modeling, analysis, design, and verifications appropriate for the different models. UTP 3.1 Designs of sequential programs 3.2 Designs of object-oriented programs 3.3 Concurrent programs 4 Models of components two kinds of actions, the interface actions K.IF and the internal actions K.iA. two kinds of abstract models of reactive program: --channel/event-based processes algebras --I/O automata two kinds of reactive programs of rCOS: -- components --processes. 4.1 Components 4.2 Refinement between closed components 4.3 Open components and component composition 4.4 Processes 5 Integrating theories, techniques, and tools into the development process 5.1 UML profile of rCOS a UML profile for rCOS: to ease the difficulty of users in creating formal models The profile defines: 1) An rCOS class declaration section ClassDecls as a UML class diagram 2) The object interactions in methods of classes as object sequence diagrams, the following models defined in the UML profile (see Fig. 9): 1) A component diagram in which each component representsa use case, 2) A class diagram or a number of class diagrams (packages) defining the classes and types of data and objects of the components, 3) A set of component-sequence diagrams represents the interactions of the components and their interactions with the actors, 4) A set of state diagrams, one for each component, 5) Local data functionality of provided methods of the components. two major design steps: 1) OO design of provided methods. 2) Generating a component-based design architecture model. 5.2 Top-down development 6 Conclusions rCOS a formal model-driven engineering method for component-based software.pdf Graph transformations for object-oriented refinement Liang Zhao, Xiaojian Liu, Zhiming Liu and Zongyan Qiu Formal Aspects of Computing (2009) 21: 103–131 Abstract. An object-oriented program consists of a section of class declarations and a main method. The class declaration section represents the structure of an object-oriented program, that is the data, the classes and relations among them. The execution of the main method realizes the application by invoking methods of objects of the classes defined in the class declarations. Class declarations define the general properties of objects and how they collaborate with each other in realizing the application task programmed as the main method. Note that for one class declaration section, different main methods can be programmed for different applications, and this is an important feature of reuse in object-oriented programming. On the other hand, different class declaration sections may support the same applications, but these different class declaration sections can make significant difference with regards to understanding, reuse and maintainability of the applications.With a UML-like modeling language, the class declaration section of a program is represented as a class diagram, and the instances of the class diagram are represented by object diagrams, that form the state space of the program. In this paper, we define a class diagram and its object diagrams as directed labeled graphs, and investigate what changes in the class structure maintain the capability of providing functionalities (or services). We formalize such a structure change by the notion of structure refinement. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is, the resulting class graph should be able to provide at least as many, and as good, services (in terms of functional refinement) as the original graph. We then develop a calculus of object-oriented refinement, as an extension to the classical theory of data refinement, in which the refinement rules are classified into four categories according to their natures and uses in object-oriented software design. The soundness of the calculus is proved and the completeness of the refinement rules of each category is established with regard to normal forms defined for object-oriented programs. These completeness results show the power of the simple refinement rules. The normal forms and the completeness results together capture the essence of polymorphism, dynamic method binding and object sharing by references in object-oriented computation. Keywords: Class graph; Object graph; Graph transformation; Normal form; Object-orientation; Structure refinement 1. Introduction formal semantics of object-oriented programs Q: it is difficult to understand and use the semantics of object-oriented programs A: -- denotational (or an axiomatic) semantics to an operational semantics rCOS 1.1. Contribution 1.2. Related work 1.3. Overview 1) Section 2 shows how a class declaration section can be defined as a directed labeled graph. 2) Sect. 3 define object graphs for a class graph to represent system states. 3) Section 4 defines structure refinements between class graphs and their derived relations between object graphs. 4) Sect. 5 introduce the concept of interface and extend the notion of structure refinements with respect to interfaces. 5) Sect. 6 provide the refinement rules for modifying methods in a class graph without changing the whole class structure. 6) Section 7 defines the normal forms and proves completeness results. 7) Sect. 8 draw the conclusions and discuss about future work. 2. Class graphs Graph transformations for object-oriented refinement.pdf rCOS: Refinement of Component and Object Systems Zhiming Liu, He Jifeng,, and Xiaoshan FMCO 2004, LNCS 3657, pp. 183–221, 2005. Abstract. We present a model of object-oriented and component-based refinement. For object-orientation, the model is class-based and refinement is about correct changes in the structure, methods of classes and the main program, rather than changes in the behaviour of individual objects. This allows us to prove refinement laws for both high level design patterns and low level refactoring. For component-based development, we focus on the separation of concerns of interface and functional contracts, leaving refinement of interaction protocols in future work. The model supports the specification of these aspects at different levels of abstractions and their consistency. Based on the semantics, we also provide a general definitional approach to defining different relational semantic models with different features and constraints. Keywords: Object-Orientation, Component-Based Development, Refinement, Specification, Consistency. 1 Introduction three axes: 1. the temporal axis 2. different aspects of the system 3. third axis is that of system evolution and maintenance the main problems: – Since the requirements specification is informal there is no way to ascertain its completeness resulting in a lot of gaps. – The gaps in requirements are filled by ad-hoc decisions taken by programmers who are not qualified for the job of requirement analysis. This results in code of poor quality. – There is no traceability between requirements and implementation making it very expensive to accommodate changes and maintain the system. – Most of the tools are for project management and system testing. Although these are useful, they are not enough for ensuring the semantic correctness of the implementation for a requirements specification and semantic consistency of changes made in the system. rCOS: a calculus of Refinement of Component and Object Systems the focus of rCOS: -- interfaces -- functional contracts -- interaction protocols a design: the organization of this paper: 1) Section 2 introduce semantic basis of the notion of designs in Unifying Theories of Programming 2) Section 3 define the model for object systems. 3) Section 4 present refinement calculus of object-oriented designs 4) Section 5 show how the model for object systems is extended to deal withcomponent systems. 5) Section 6 conclude the article with discussion and related work. 2 Semantic Basis modelling the execution of a program in terms of a relation between the states of the program one of the core ideas of the UTP:what to observe in different kinds of systems? 2.1 Programs as Designs the goal of this subsection: how the basic programming constructs can be defined as designs? define the meaning of primitive commands program commands as framed designs in Table 1. 2.2 Refinement of Designs 3 Object Systems the goal of this section: introduce to the syntax and semantics of rCOS for object systems 3.1 Syntax 3.2 Semantics 3.3 Evaluation of Expressions The evaluation results of expressions are given in Table. 2 4 Object-Oriented Refinement three kinds of refinement: 1. Refinement relation between object systems. 2. Refinement relation between declaration sections (structural refinement). 4.1 Refinement of Object Systems 4.2 Structure Refinement 4.3 Laws of Structural Refinement 5 Component Systems author's idea: a contract-oriented approach to the specification, design and composition of components the open issues: -- Finding appropriate formal approaches for specifying components --the architectures for composing them -- the methods for component-based software construction 5.1 Introduction 5.2 Interfaces -- Merge Interfaces -- 5.3 Contracts a contract: a functional specification of an interface 5.4 Component 5.5 Semantics Components 5.6 Refinement and Composition of Components 6 Conclusion 6.1 Related Work 6.2 Future Work rCOS Refinement of Component and Object Systems.pdf Refinement of Models of Software Components Zizhen Wang and Hanpin Wang, Naijun Zhan ACM SAC’10 March 22-26, 2010, Sierre, Switzerland ABSTRACT Models of software components at different levels of abstraction, component interfaces, contracts, implementations and publications are important for component-based design. Refinement relations among models at the same level and between different levels are essential for model-driven development of components. Classical refinement theories mainly focus on verification and put little attention on design. Therefore, most of them are not suitable for component-based model-driven development (CB-MDD). To address this issue, in this paper, we propose two refinement relations for CB-MDD, that is a trace-based refinement and a state-based refinement. Both are discussed in the framework of rCOS, which is a formal model of component and object systems. These refinement relations provide different granularity of abstraction and can capture the intuition that a refined component provides “more” and “better” services to the environment. We also show how to extend these refinement relations to allow us to compare contracts, components and publications with different interfaces by exploiting the primitive operator internalizing over contracts, components and publications. Keywords : CB-MDD, data refinement, trace refinement, rCOS 1. INTRODUCTION Component-based model-driven development (CB-MDD) basic idea: to compose/decompose a complicated system from/into some simpler ones with well-defined interfaces used for communication across the components. different abstraction levels of software components: -- component interfaces -- contracts -- implementations -- publications rCOS the contributions of this paper include: • Firstly, a trace-based refinement is defined. • Secondly, propose a state-based refinement relation The rest of this paper is organized as: 1) Section 2 review some basic notions; 2) Section 3 presents trace refinement and data refinement on contracts. 3) Section 4 considers the notions of trace refinement and data refinement on components. 4) Section 5 propose alternating trace refinement and alternating data refinement on publications 5) Section 6 is devoted to extending these refinement relations to compare contracts, components and publications with different interfaces. 6) Section 7 concludes this paper. 2. BASIC NOTIONS 2.1 Design UTP 2.2 Refinement of design 2.3 Reactive design and guarded design 3. TRACE REFINEMENT AND DATA REFINEMENT OF CONTRACTS 3.1 Trace refinement two principles towards refinement of components in CB-MDD 3.2 Data refinement 4. TRACE REFINEMENT AND DATA REFINEMENT OF COMPONENTS 5. ALTERNATING TRACE (DATA) REFINEMENT OF PUBLICATIONS 6. DIFFERENT INTERFACES the outline of this paper: -- first briefly review the primitive operators over components and publications -- Then prove these operators except for internalizing preserve these refinement relations -- finally we show how to exploit the internalizing operator to extend the refinement relations to compare contracts, components and publications with different interfaces. 6.1 Primitive operators 7. CONCLUSION AND FUTUREWORK Refinement of models of software components.pdf rCos tutorial slide: rCos ICTAC09-tutorial-slides.pdf rCos Slides-rCOS part II.pdf rCos Slides-SE.pdf rCOS-Profile.pdf Unblockable Compositions of Software Components Ruzhen Dong, Johannes Faber, Zhiming Liu,Jirí Srba,Naijun Zhan,Jiaqi Zhu CBSE’12, June 26–28, 2012, Bertinoro, Italy ABSTRACT We present a new automata-based interface model describing the interaction behavior of software components. Contrary to earlier component- or interface-based approaches, the interface model we propose specifies all the non-blockable interaction behaviors of a component with any environment. To this end, we develop an algorithm to compute the unblockable interaction behavior, called the interface model of a component, from its execution model. Based on this model, we introduce composition operators for the components and prove important compositionality results, showing the conditions under which composition of interface models preserves unblockable sequences of provided services. Keywords: Component-based design, interface theory, composition 1. INTRODUCTION component-based software engineering - component - interface a component: --a provided interface: which executions of services the component offers to its environment -- a required interface: what services the component needs to call in order to provide the services on its provided interface execution model - non-deterministic interface model: Related work: -- the I/O Automata -- actions: input, output, and internal actions -- the Interface Automata Input/Output (I/O) Automata: Summary of contributions. The contributions of this paper are (1) a new interface model ensuring unblockable compositions of software components; (2) an algorithm to generate the interface model of a component based on its execution model; (3) definitions of basic operations used in component-based design; (4) a formal analysis showing that unblockable behavior is preserved for the complete plugging of components. Outline of the paper. The rest of the paper is organized as follows. 1)Sect. 2 introduce component automata and an algorithmic way to generate their interface models. 2)Sect. 3present the composition operators to compose components and prove important properties for these operators. 3)Sect. 4conclude the paper and discuss the future work. 2. COMPONENT AUTOMATA the outline of this section: -- first introduce some notions that will be used throughout the paper --then motivate component automata and component interface automata. -- At last,give an algorithm transforming component automata to component interface automata and prove its correctness. 2.1 Preliminary Definitions 2.2 Execution Model of a Component 2.3 Unblockable Equivalence 2.4 Interface Model of a Component A general construction of an interface automaton I(C) for a given component automaton C is given in Algorithm 1 3.2 Composition of Interface Models 3. COMPOSITION OPERATORS operator: -- the product --the plugging of components 3.1 Product of Component Automata 4. CONCLUSION AND FUTUREWORK author's work: -- a formal model for component interfaces that guarantees unblockable composition of software components -- provided an algorithm to compute the unblockable interface from a component’s execution model. -- introduced the operators of composition and plugging open problem: -- -- interface models with timing characteristics Unblockable compositions of software components.pdf I comment: Ensemble Engineering and Emergence Hu Jun, Zhiming Liu, G.M. Reed, and J.W. Sanders Software-Intensive Systems, LNCS 5380, pp. 162–178, 2008 Abstract. The complex systems lying at the heart of ensemble engineering exhibit emergent behaviour : behaviour that is not explicitly derived from the functional description of the ensemble components at the level of abstraction at which they are provided. Emergent behaviour can be understood by expanding the description of the components to refine their functional behaviour; but that is infeasible in specifying ensembles of realistic size (although it is the main implementation method) since it amounts to consideration of an entire implementation. This position paper suggests an alternative. ‘Emergence’ is clarified using levels of abstraction and a method proposed for specifying ensembles by augmenting the functional behaviour of its components with a system-wide ‘emergence predicate’ accounting for emergence. Examples are given to indicate how conformance to such a specification can be established. Finally an approach is suggested to Ensemble Engineering, the relevant elaboration of Software Engineering. On the way, the example is considered of an ensemble composed of artificial agents and a case made that there emergence can helpfully be viewed as ethics in the absence of free will. 1 Introduction ensembles 2 Ensembles 2.1 Levels of Abstraction 2.2 Emergence 2.3 Ensembles 2.4 Reductionism 2.5 Related Approaches 3 Examples 3.1 Coin Tossing Ensemble Engineering and Emergence.pdf 面向服务架构中服务实现的策略 刘 静 何积丰 Zhiming Liu 中国科学 E 辑 信息科学 2006, 36(10): 1220~1239 摘要 构造了层次化的SOA 模型, 并提出了将服务使用层与服务实现层分层处理的策略. 建立了基于服务的构件模型来实现SOA 中的服务, 使用接口来描述服务的语法, 契约来描述服务的语义, 并用卫式设计来模服务的行为. 将接口作为结合构件技术与面向服务架构的关键. 用实例说明了如何使用这种方法来实现面向服务的设计. 此工作为利用构件技术解决面向服务架构中的服务实现 问题奠定了基础. 关键词： 面向服务 接口 契约 构件 面向服务计算(service-oriented computing, 简称SOC) 构件 -〉services 不同模块连接起来的主要问题为: ● 缺乏标准语法, 而标准语法可以明确(无歧异)地表达所有系统信息; ● 缺乏标准语义模型, 而标准语义模型使得企业可以用一致的语言来表达其业务; ● 缺乏标准的协议, 而标准的协议是不同操作环境、不同企业之间消息传递的基础; ● 缺乏绑定事务文档与行为的标准程式. author's idea: 基于统一程序理论(unifying theories of programming,UTP), 用Java 风格的对象系统精化演算语言(refinement calculus of object systems,rCOS)描述了服务的语法、语义, 并构造了面向服务的构件模型. -- 先分析构件应提供的服务 -- 再将服务分配到接口 --用接口来描述服务的语法 -- 引入契约来表达服务的语义, 通过模型转换技术来保证服务实现的正确性. 1 方法概述 SOA 模型. 顶层主要是管理服务使用, 而另一层则是服务实现, 如图1 所示 实现服务: ● 使用WSDL 描述服务, 然后将其转换为UML 模型. ● 使用rCOS 描述服务规范, 得到服务的一个精确语义模型. ● 使用管理构件来管理执行构件. 管理构件按照服务规范的要求把任务委托给执行构件并把构件组合成一个闭合构件. ● 使用执行构件来实现管理构件所委托的功能. 2 面向服务的构件模型 构件接口: 描述在构建和维护软件系统的过程中构件与外界交互时需要什么. -- 语法规范 -- 语义定义 2.1 接口 接口: 构件访问点的语法规范 2.2 契约 契约: 描述接口的语义. 2.3 构件 构件: 契约的实现 2.4 组合 3 应用: 电子商店 3.1 接口 3.2 契约 3.3 构件 3.4 组合 4 结论与讨论 4.1 结论 面向服务架构中服务实现的策略.pdf 3 Sun Meng Towards the Introduction of QoS Information in a Component Model Sun Meng, Luis S. Barbosa SAC’10 March 22-26, 2010, Sierre, Switzerland ABSTRACT Assuring Quality of Service (QoS) properties is critical in the development of component-based distributed systems. This paper presents an approach to introduce QoS constraints into a coalgebraic model of software components. Such constraints are formally captured through the concept of a Q-algebra which, in its turn, can be smoothly integrated in the definition of component combinators. Keywords: Component-based design, coalgebra, QoS properties 1. INTRODUCTION components - services - Quality of Service (QoS) The purpose of this paper: suggests how a formal calculus for component composition can be extended in order to take into account, in an explicit way, QoS information The calculus is based on a coalgebraic model Q-algebra 2. COMPONENTS AS COALGEBRAS Software components: dynamic systems +public interface +private, encapsulated state. generic components- coalgebras Question: how do they get composed and what kind of calculus emerges from this framework ? 3. INTRODUCING QOS IN THE COMPOENT MODEL Q-algebra 4. CONCLUSIONS Towards the introduction of QoS information in a component model.pdf 4 others 一种基于构件演算的主动构件精化方法 陈鑫 Journal of Software, Vol.19, No.5, May 2008, pp.1134−1148 摘要: 现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性. 关键词: 接口;构件;语义;契约;精化;组合 构件 - 正确性的验证 - correct-by-construction - 精化: 转换一步步地从规约构造出正确的最终实现 difficulty: 面向构件系统的精化理论和方法 主动构件 vs. 反应式构件 -- 主动构件: -- 反应式构件: 一种以被动方式工作的构件 构件技术研究重要内容: 如何为主动构件构造一形式化模型,刻画和分析主动构件行为,为主动构件组装提供形式化支撑 构件演算: 以设计演算为基础,建立反应式构件的形式化模型,研究反应式构件的精化方法和组装方法. its drawbacks: -- 构件演算没提供直接描述主动构件自主行为的形式化机制 -- 也未能给出分析自主行为如何影响主动构件交互行为的方法 author's work: 给出主动构件的行为模型,研究了主动构件的精化方法. -- 首先,在接口的形式模型“契约”中加入对自主方法描述.契约用卫式设计定义接口中公共方法和自主方法的功能规约. -- 分析契约交互行为的非确定性,通过协议和一对发散、失败集合来描述契约的交互行为,给出了计算协议和发散、失败集合的方法.同时,用这对发散、失败集合上的包含关系定义契约的精化关系,证明应用仿真技术判定契约精化关系的定理. -- 构件的语义定义成一个映射其需求接口的契约到其服务接口的契约的函数.以此为基础,可以应用契约之间的精化关系来研究构件间的精化关系. -- 给出支持构件组装方法的形式规则.综合运用精化和组装的方法,可以在构件系统自底向上的过程中保证系统的正确性. the organization of this paper: 1) 第1节介绍本文工作的基础——构件演算,并通过一个实例分析构件演算在分析主动构件时遇到的问题. 2) 第2节给出主动构件形式模型的定义,并以此为基础研究主动构件的精化方法和组装方法. 3) 第3节与相关工作做比较. 4) 第4节总结全文并对今后的工作进行展望. 1 构件演算 统一程序设计理论: 设计(design): -- 将一个程序的执行描述为关于程序状态空间的一个关系. -- 程序的状态空间定义在一组变量之上,这组变量记作α. -- 程序的一个状态就是从这组变量到变量值空间的一个映射. 最弱前提条件的演算方法 -- 定义2给出最弱前提条件和设计之间的关系. 引入反应式设计: Q: A: 引入卫式条件来控制方法的可用性,方法是可用的当且仅当卫式条件为真. 构件演算: 契约层和构件层两个层次构造反应式构件的形式模型 -- 契约层: 引入契约描述接口的行为,契约用卫式设计定义接口中方法的功能规约,用协议约束环境对接口方法的调用顺序. 契约的动态交互行为定义在一对发散、失败集合上 -- 构件演算将构件的语义定义: 接口: 构件和外界环境交互的设施,构件演算定义了如下标准形式的接口. 契约: 2 主动构件的形式模型和精化方法 Q: 主动构件的行为建模时,需解决两个问题: -- 一是如何建立构件自主行为的直接描述机制, -- 二是在为构件交互行为建模时,如何分析自主行为对构件交互行为的影响. author's idea: -- 接口层 -- 构件层 2.1 接口的形式化模型和精化方法 引入契约定义接口的语义. 将契约的动态行为定义在包含参数的方法调用和方法返回事件序列之上. 2.2 构件的形式化模型和精化方法 2.3 构件的组装 构件的组装过程: -- 两个构件各自在对方的服务接口中寻找可与自己的需求相匹配的方法,并将它们连接起来. -- 运行时刻,构件双方需要在相连方法的调用和返回事件上同步.即当函数调用发生时,发出调用方的调用事件需要与接受调用方的接受事件同步; -- 函数返回时,接受调用方的返回事件需与发出调用方的接受事件同步. 3 相关工作 challenges: 主动构件形式化模型 -- -- Reo -- 4 总结及展望 future work: -- + time model -- CORBA 一种基于构件演算的主动构件精化方法.pdf Unifying Theories of Programming C.A.R.Hoare, He Jifeng Prentice Hall 1998 Chapter 0 Challenge of Unification three independent axes of theories of programming -- structure -- the level of abstraction -- mathematical technique 0.1 Programming paradigms -- imperative -- functional -- logical -- parallel 0.2 Levels of abstraction 0.3 Varieties of presentation -- denotational -- algebraic -- operational 0.4 Alphabets 0.5 Signuatures 0
Paper: Formal semantics of UML state diagram and automatic verification Based on Kripke structure Author: Yefei Zhao, Zongyuan Yang, Jinkui Xie Abstract: If UML is formalized with dynamic semantics, automatic verification can be performed for system model in the early stage of software procedure. It becomes more and more important to apply model checking in UML, such that software architecture can be formalized with dynamic semantics. We explicitly proposed the mapping rules between UML state diagram and Kripke structure semantics. UML state diagram is mapped to the value transition of variable rather than the transition of states, thus the situation in that system finite state automata cant be exhausted can be resolved. Finally, a critical resource competition example is illustrated according to the theory. The mapping rules we proposed are bi-direction, as a result, the theory can be applied in both forward software engineering in design phase and reverse software engineering in implementation phase. Published in Conference: 22nd IEEE Canadian Conference on Electrical and Computer Engineering (CCECE 2009)(EI index) Date: May, 2009
标签: UML
