Publications
202 results found
Karamanolis C, Giannakopoulou D, Magee JN, et al., 2000, Model Checking of Workflow Schemas, Proceedings of 4th Intl. Conferemce on enterprise Distributed Object Computing (EDOC), Makuhari, Japan
Magee JN, Pryce N, Giannakopoulou D, et al., 2000, Graphical Animation of Behaviour Models, Proceedings 22nd International Conference on Software Engineering, Limerick, Ireland, Pages: 499-508
Uchitel S, Chatley R, Kramer J, et al., 2000, The labelled transition system analyzer and plugins
Van Ommering R, Van Der Linden F, Kramer J, et al., 2000, The Koala Component Model for Consumer Electronics Software, IEEE Computer, Vol: 33, Pages: 78-85
Magee J, Kramer J, Nuseibeh B, 2000, Hybrid model visualization in requirements and design: A preliminary investigation, 10th International Workshop on Software Specification and Design, Publisher: IEEE COMPUTER SOC, Pages: 3-9
- Author Web Link
- Cite
- Citations: 62
Kramer J, Magee JN, Ng K, et al., 2000, Software Architecture Description, Software Architecture for Product Families: Principles and Practice, Editors: Van Der Linden, Jazayeri, Van Der Linden, Jazayeri, Van Der Linden, Jazayeri, Publisher: Addison Wesley
Magee JN, Kramer J, 1999, Concurrency - State Models and Java Programs, Publisher: John Wiley & Sons
Karamanolis C, Giannakopoulou G, Magee J, et al., 1999, Modelling and analysis of workflow processes, Departmental Technical Report: 99/2, Publisher: Department of Computing, Imperial College London
Practical experience indicates that the definition of real-world workflow applications is a complex and error-prone process. Existing workflow management systems provide the means, in the best case, for very primitive syntactic verification, which is not enough to guarantee the overall correctness and robustness of workflow applications. The paper introduces a method for formal verification of workflow schemas (definitions).Workflow behaviour is modelled by means of an automata-based method, which facilitates exhaustive compositional reachability analysis. The workflow behaviour is checked against both safety and liveness properties, which can be either generic (applicable to all workflow schemas) or domain specific (applicable to a given schema). The analysis is performed by automated tools, which are accessible to designers who are not experts in formal methods.
Giannakopoulou D, Magee J, Kramer J, 1999, Fairness and priority in progress property analysis, Departmental Technical Report: 99/2, Publisher: Department of Computing, Imperial College London
The liveness characteristics of a system are intimately related to the notion of fairness. However, the task of modelling explicitly fairness constraints is complicated in practice. To address this issue, we propose to check LTS (Labelled Transition System) models under a strong fairness assumption, which can be relaxed with the use of action priority. The combination of the two provides a novel and practical way of dealing with fairness. The approach is presented in the context of a class of liveness properties termed progress, for which it yields an efficient model-checking algorithm. Progress properties cover a wide range of interesting properties of systems, while presenting a clear intuitive meaning to users. An extensive comparison is provided of the approach proposed with classical LTL model-checking.
Magee JN, 1999, Behavioral Analysis of Software Architectures using LTSA, Proceedings of 21st IEEE International Conference on Software Engineering (ICSE-21), Los Angeles, USA
Kramer J, Magee JN, 1999, Modelling for mere Mortals, Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), Amsterdam
Giannakopoulou D, Magee JN, Kramer J, 1999, Checking Progress with Action Priority: Is it Fair?, 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering / 7th European Software Engineering Conference (FSE / ESEC '99), Toulouse, Publisher: Springer-Verlag, Pages: 511-528
Giannakopoulou D, Magee JN, Kramer J, 1999, Checking Progress with Action Priority: Is it Fair?, 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering / 7th European Software Engineering Conference (FSE / ESEC '99), Toulouse, Publisher: Springer-Verlag, Pages: 511-528
Giannakopoulou D, Magee J, Kramer J, 1999, Checking progress with action priority: Is it fair?, 7th European Software Engineering Conference/7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Publisher: SPRINGER-VERLAG BERLIN, Pages: 511-527, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 10
Kramer J, Magee JN, 1999, Modelling for mere Mortals, Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), Amsterdam
Magee J, Kramer J, Giannakopoulou D, 1999, Behaviour analysis of software architectures, 1st Working IFIP Conference on Software Architecture (WICSA1), Publisher: KLUWER ACADEMIC PUBLISHERS, Pages: 35-49, ISSN: 1571-5736
- Author Web Link
- Cite
- Citations: 46
Magee JN, Kramer J, Giannakopoulou D, 1999, Behaviour Analysis of Software Architectures, First Working IFIP Conference on Software Architecture (WICSA1), San Antonio, Texas, Publisher: Kluwer Academic Pub., Pages: 35-50
Kramer J, Magee JN, 1998, Analysing Dynamic Change in Distributed Software Architectures, IEE Proceedings - Software, Vol: 145, Pages: 146-154
Leonhardt U, Magee JN, 1998, Security Considerations for a Distributed Location Service, Journal of Network and Systems Management, Vol: 6
Karamanolis C, Magee JN, 1998, Construction and Management of Highly Available Services in Open Distributed Systems, Distributed Systems Engineering Journal, Vol: 5
Giannakopoulou D, Magee J, Kramer J, 1998, Checking progress with aAction priority: is it fair?, Departmental Technical Report: 98/2, Publisher: Department of Computing, Imperial College London
The liveness characteristics of a system are intimately related to the notion of fairness. However, the task of explicitly modelling fairness constraints is complicated in practice. To address this issue, we propose to check LTS (Labelled Transition System) models under a strong fairness assumption, which can be relaxed with the use of action priority. The combination of the two provides a novel and practical way of dealing with fairness. The approach is presented in the context of a class of liveness properties termed progress, for which it yields a particularly efficient model-checking algorithm. Progress properties cover a wide range of interesting properties of systems, while presenting a clear intuitive meaning to users.
Magee J, Kramer J, Giannakopoulou D, 1998, Software Architecture directed behaviour analysis, 9th International Workshop on Software Specification and Design, Publisher: IEEE COMPUTER SOC, Pages: 144-146
- Author Web Link
- Cite
- Citations: 3
Magee JN, Kramer J, Giannakopoulou D, 1998, Software Architecture directed Analysis, 9th IEEE International Workshop on Software Specification and Design (IWSSD 9) Japan, Pages: 144-146
Leonhardt U, Magee J, 1998, , Journal of Network and Systems Management, Vol: 6, Pages: 51-70, ISSN: 1064-7570
Kramer J, Magee JN, 1998, Analysing Dynamic Change in Distributed Software Architectures: A Case Study, IEEE 4th International Conference on Configurable Distributed Systems, (CDS 98), Annapolis, Pages: 91-100
Kramer J, Magee JN, 1998, Distributed Software Architectures: Tutorial, 20th IEEE Int. Conference On Software Engineering (ICSE-20), Kyoto, Pages: 280-281
Kramer J, Magee JN, 1998, Analysing Dynamic Change in Distributed Software Architectures: A Case Study, IEEE 4th International Conference on Configurable Distributed Systems, (CDS 98), Annapolis, Pages: 91-100
Magee JN, Kramer J, 1998, Composing Distributed Objects in CORBA, Information Systems Interoperability, Editors: Kramer, Papzoglou, Schmidt, Kramer, Papzoglou, Schmidt, Publisher: Research Studies Press
Leonhardt U, Magee JN, 1998, Multi-Sensor Location Tracking, Proceedings of 4th ACM/IEEE International Conference on Mobile Computing and Networking, Dallas, Pages: 203-214
Kramer J, Magee J, 1997, Exposing the skeleton in the coordination closet, Pages: 18-31, ISSN: 0302-9743
One of the ways in which we cope with large and complex systems is to abstract away some of the detail, considering them at an architectural level as compositions of interacting components. To this end, the variously termed Coordination, Configuration and Architectural Description Languages (ADL) facilitate description, comprehension and reasoning at that level, providing a clean separation between individual component behaviour and their interaction in a software architecture. However, in the search to provide sufficient detail for reasoning, analysis or construction, many approaches are in danger of obscuring the essential structural aspect of the architecture, thereby losing the benefit of abstraction. In this paper we argue for the use of a concise and simple language explicitly designed for describing architectural structures. This can be used to provide the "skeleton" upon which to add the particular details of concern when necessary. Systems described in this way have an explicit and exposed skeleton which, being shared, helps to maintain consistency between the various elaborated views. To illustrate our approach, we use the Darwin architectural description language and the Tracta approach for compositional reachability analysis.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.