%Aigaion BibTeX export %Sunday 23rd of March 2008 12:02:03 PM @INPROCEEDINGS {DBLP:conf/sofsem/ChenLM07, title = {Separation of Concerns and Consistent Integration in Requirements Modelling}, author = {Chen, Xin and Liu, Zhiming and Mencl, Vladimir}, crossref = {DBLP:conf/sofsem/2007}, year = {2007}, pages = {819--831}, url = {http://dsrg.mff.cuni.cz/publications/XinLiuMencl-SOFSEM07-ConsistentRequirements.pdf}, doi = {10.1007/978-3-540-69507-3_71}, abstract = {Due to their increasing complexity, design of software systems is not becoming easier. Furthermore, modern applications ranging from enterprise to embedded systems require very high levels of correctness and dependability assurance. The most effective means to handle complexity is separation of concerns and incremental development, and assurance of correctness requires formal modelling and formal analysis. When separation of concerns splits the model into several parts, an important issue is to ensure consistency among these parts. We propose an approach supporting separation of concerns and consistent and incremental modelling of requirements.}, } @ARTICLE {DBLP:journals/tcs/HeLL06, title = {{rCOS}: A refinement calculus of object systems}, author = {He, Jifeng and Liu, Zhiming and Li, Xiaoshan}, journal = {Theor. Comput. Sci.}, year = {2006}, volume = {365}, number = {1-2}, pages = {109--142}, note = {UNU-IIST TR 322}, url = {http://rcos.iist.unu.edu/publications/TCSpreprint.pdf}, doi = {10.1016/j.tcs.2006.07.034}, keywords = {Object Orientation, Refinement, Semantics, UTP}, abstract = {This article presents a mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language can be used to specify object-oriented designs as well as programs. We present a calculus that supports both structural and behavioral refinement of object-oriented designs. The design calculus is based on the predicate logic in Hoare and He's Unifying Theories of Programming (UTP).}, } @INPROCEEDINGS {DBLP:conf/fsen/ChenHLZ07, title = {A Model of Component-Based Programming}, author = {Chen, Xin and He, Jifeng and Liu, Zhiming and Zhan, Naijun}, crossref = {DBLP:conf/fsen/2007}, year = {2007}, pages = {191--206}, note = {UNU-IIST TR 350}, url = {http://www.iist.unu.edu/newrh/III/1/docs/techreports/report350.pdf}, doi = {10.1007/978-3-540-75698-9_13}, abstract = {Component-based programming is about how to create application programs by prefabricated components with new software that provides both glue between the components, and new functionality. Models of components are required to support black-box compositionality and substitutability by a third party as well as interoperability. However, the glue codes and programs designed by users of the components for new applications in general do not require these features, and they can be even designed in programming paradigms different from those of the components. In this paper, we extend the rCOS calculus of components with a model for glue programs and application programs that is different from that of components. We study the composition of a glue program with components and prove that components glued by a glue program yield a new component.}, } @ARTICLE {DBLP:journals/entcs/LiuLZ07, title = {Object-Oriented Structure Refinement - A Graph Transformational Approach}, author = {Liu, Xiaojian and Liu, Zhiming and Zhao, Liang}, journal = {Electr. Notes Theor. Comput. Sci.}, year = {2007}, volume = {187}, pages = {145--159}, note = {UNU-IIST TR 340}, url = {http://www.iist.unu.edu/newrh/III/1/docs/techreports/report340.pdf}, doi = {10.1016/j.entcs.2006.08.049}, abstract = {In UML, the general structure of objects, their attributes and relations are modeled as a class graph, and an instance of a class graph is defined as an object graph. The class graph of a system determines the general properties of objects and how objects collaborate in realizing a use case. In this paper, we define class graphs and their object graphs as directed labelled graphs, and investigate in a graph theoretical approach what changes in the object structure maintain the capability of providing services. We define the general notion of structure refinements. 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 well as the original graph. We give a small set of structure refinement rules that is proved to be sound and complete for a kind of structure refinement.}, } @INPROCEEDINGS {DBLP:conf/birthday/ChenLLSY07, title = {Harnessing {rCOS} for Tool Support - The {CoCoME} {Experience}}, author = {Chen, Zhenbang and Li, Xiaoshan and Liu, Zhiming and Stolz, Volker and Yang, Lu}, crossref = {DBLP:conf/birthday/2007bz}, booktitle = {Formal Methods and Hybrid Real-Time Systems}, year = {2007}, pages = {83--114}, note = {UNU-IIST TR 383}, url = {http://www.iist.unu.edu/newrh/III/1/docs/techreports/report343.pdf}, doi = {10.1007/978-3-540-75221-9_5}, abstract = {Software development tools need to support more and more phases of the entire development process, because applications must be developed more correctly and efficiently. The tools therefore need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensure high quality of such add-ins is to base them on sound formal foundations. In order to know where such add-ins will fit, we investigate the use of an existing successful commercial tool and identify suitable places for adding formally supported checking, transformation and generation modules. The paper concludes with a discussion of feasibility of developing the proposed add-ins and how to give conditions such that they will actually be used.}, } @INPROCEEDINGS {DBLP:conf/iceccs/ChenLSYR07, title = {A Refinement Driven Component-Based Design}, author = {Chen, Zhenbang and Liu, Zhiming and Stolz, Volker and Yang, Lu and Ravn, Anders P. }, crossref = {DBLP:conf/iceccs/2007}, year = {2007}, pages = {277--289}, url = {http://www.iist.unu.edu/~yanglu/documents/iceccs07.pdf}, doi = {10.1109/iceccs.2007.12}, abstract = {odern software applications ranging from enterprise to embedded systems are becoming increasingly complex, and require very high levels of dependability assurance. The most effective means to handle complexity is separation of concerns and incremental development, and assurance of dependability requires formal methods. We report here our experience on these issues in an application of a formal calculus, rCOS, to a component-based design of the point of sale system (POS). We demonstrate the possibility in scaling-up correctness by design and discuss how rCOS may be integrated with current and emerging software engineering tools.}, } @INPROCEEDINGS {DBLP:conf/ictac/JifengLL05, title = {Component-Based Software Engineering}, author = {He, Jifeng and Li, Xiaoshan and Liu, Zhiming}, crossref = {DBLP:conf/ictac/2005}, year = {2005}, pages = {70--95}, note = {UNU-IIST TR 330}, url = {http://www.iist.unu.edu/newrh/III/1/docs/techreports/report330.pdf}, doi = {10.1007/11560647_5}, keywords = {Components,Interfaces,Contracts,Protocols,Functionality,Consistency,Composition,Refinement,Simulation}, abstract = {We discuss some of the difficulties and significant issues that we need to consider when developing a formal method for component-based software engineering. We argue that to deal with the challenges, there is a need in research to link existing theories and methods of programming for effective support to component-based software engineering. We then present our initiative on a unified multi-view approach to modelling, design and analysis of component systems, emphasising the integration of models for different views.}, } @ARTICLE {facs07, title = {Graphtransformations for object-oriented refinement}, author = {Zhao, Liang and Liu, Xiaojian and Liu, Zhiming and Qiu, Zongyan}, journal = {Formal Aspects of Computing}, year = {2008}, issn = {1433-299X}, doi = {10.1007/s00165-007-0067-y}, 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 de 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 offour 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.}, } %Crossreferenced publications: @PROCEEDINGS {DBLP:conf/sofsem/2007, title = {SOFSEM 2007: 33rd Conference on Current Trends in Theory and Practice of Computer Science}, editor = {van Leeuwen, Jan and Italiano, Giuseppe F. and van der Hoek, Wiebe and Meinel, Christoph and Sack, Harald and Plasil, Frantisek}, booktitle = {SOFSEM 2007: 33rd Conference on Current Trends in Theory and Practice of Computer Science}, series = {Lecture Notes in Computer Science}, year = {2007}, mon = {January}, volume = {4362}, publisher = {Springer}, address = {Harrachov, Czech Republic}, isbn = {978-3-540-69506-6}, } @PROCEEDINGS {DBLP:conf/fsen/2007, title = {International Symposium on Fundamentals of Software Engineering (FSEN 2007)}, editor = {Arbab, Farhad and Sirjani, Marjan}, booktitle = {International Symposium on Fundamentals of Software Engineering (FSEN 2007)}, series = {Lecture Notes in Computer Science}, year = {2007}, month = {April}, volume = {4767}, publisher = {Springer}, isbn = {978-3-540-75697-2}, } @PROCEEDINGS {DBLP:conf/birthday/2007bz, title = {Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj{\o}rner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007}, editor = {Jones, Cliff B. and Liu, Zhiming and Woodcock, Jim}, booktitle = {Formal Methods and Hybrid Real-Time Systems}, series = {Lecture Notes in Computer Science}, year = {2007}, = {4700}, publisher = {Springer}, isbn = {978-3-540-75220-2}, bibsource={DBLP, http://dblp.uni-trier.de}, } @PROCEEDINGS {DBLP:conf/iceccs/2007, title = {12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007)}, booktitle = {12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007)}, year = {2007}, month = {July}, publisher = {IEEE Computer Society}, isbn = {978-0-7695-2895-3}, } @PROCEEDINGS {DBLP:conf/ictac/2005, title = {Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium}, editor = {Hung, Dang Van and Wirsing, Martin}, booktitle = {Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium}, series = {Lecture Notes in Computer Science}, year = {2005}, month = {October}, volume = {3722}, publisher = {Springer}, address = {Hanoi, Vietnam}, isbn = {3-540-29107-5}, }