Abstract
Within a design process, the evaluation of a candidate design solution against a set of requirements may be hard, especially when the requirements concern dynamic properties. For a component-based design, evaluation of the dynamics can be based on dynamic properties of the components, and the way in which they are connected. In this paper an automated approach to the evaluation of dynamic properties of a component-based design is presented. A declarative temporal modelling language to specify and analyse dynamic properties is offered. An executable subset of this language is defined, based on ‘leads to’ relations. If executable specifications in terms of leads to relations of dynamic properties of the (reusable) components within a component-based design are available, then automated support is offered for: (1) simulation of the overall dynamics based on the executable dynamic properties of the components, (2) evaluation of requirements in the form of required overall dynamic properties of a design against a number of execution traces of the design, and (3) proving properties of an overall component-based design from executable properties of its components. The paper presents methods, techniques and software for such support and illustrates these by an example from the application area of component-based software design.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Al-Asaad, H and Hayes, JP: 1995, Design verification via simulation and automatic test pattern generation, International Conference on Computer-Aided Design, IEEE Society Press, Los Alamitos, CA, pp. 174–180.
Barringer, H, Fisher, M, Gabbay, D, Owens, R and. Reynolds, M: 1996, The Imperative Future: Principles of Executable Temporal Logic,Research Studies Press Ltd. and John Wiley and Sons.
Bouajjani, A, Lakhnech, Y and Yovine, S: 1996, Model checking for extended timed temporal logic, Proceedings of the 4th International Symposium Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT’96, Springer-Verlag, Berlin, pp. 306–326.
Brazier, FMT, Jonker, CM and Treur, J: 1998, Principles of compositional multi-agent system development, in J Cuena (ed.), Proceedings of the 15th IFIP World Computer Congress, WCC’98, Conference on Information Technology and Knowledge Systems, 1TandKNOWS’98, pp. 347–360. To be published by IOS Press, 2002.
Clarke, EM, Grumberg, O and Peled, DA: 2000, Model Checking, MIT Press, Cambridge, MA.
Dastani, M, Jonker, CM and Treur, J: To appear, A requirement specification language for configuration dynamics of multi-agent systems, in M Wooldridge, G Weiss and P Ciancarini, (eds), Proceedings of the 2nd International Workshop on Agent-Oriented Software Engineering, AOSE’01. Lecture Notes in Computer Science, vol. 2222. Springer Verlag.
Fisher, M: 1994, A survey of concurrent METATEM–the language and its applications, in DM Gabbay and HJ Ohlbach (eds), Temporal Logic — Proceedings of the First International Conference, Lecture Notes in AI, vol. 827, pp. 480–505.
Henzinger, T, Nicollin, X, Sifakis, J and Yovine, S: 1994, Symbolic model checking for real-time systems, Information and Computation 111 (2): 193–244.
Herlea, DE, Jonker, CM, Treur, J and Wijngaards, NJE: 1999, Specification of behavioural requirements within compositional multi-agent system design, in FJ Garijo and M Boman (eds), Multi-Agent System Engineering, Proceedings of the 9th European Workshop on Modelling Autonomous Agents in a Multi-Agent World, MAAMAW’99. Lecture Notes in Al, vol. 1647, Springer Verlag, Berlin, pp. 8–27.
Hölldobler, S and Thielscher, M: 1990, A new deductive approach to planning, New Generation Computing 8: 225–244.
Jonker,-CM and Treur, I: 1998, Compositional verification of multi-agent systems: a formal analysis of pro-activeness and reactiveness, in W.P. de Roever, H. Langmaack, A. Pnueli (eds), Proceedings of the International Workshop on Compositionality, COMPOS’97. Lecture Notes in Computer Science, vol. 1536, Springer Verlag, Berlin, pp. 350–380, Extended version in International Journal of Cooperative Information Systems. In press, 2002.
Kowalski, R and Sergot, M: 1986, A logic-based calculus of events, New Generation Computing 4: 67–95.
Manna, Z and Pnueli, A: 1995, Temporal Verification of Reactive Systems: Safety. Springer Verlag, Berlin.
McCarthy, J and Hayes, P: 1969, Some philosophical problems from the standpoint of artificial intelligence, Machine Intelligence 4: 463–502.
Reiter, R: 2001, Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems, MIT Press, Cambridge, MA.
Roever, WP de, Langmaack, H and Pnueli, A, (eds): 1998, Proceedings of the International Workshop on Compositionality, COMPOS’97. Lecture Notes in Computer Science, vol. 1536, Springer Verlag, Berlin.
Stirling, C: 2001, Modal and Temporal Properties of Processes, Springer Verlag, Berlin.
Yovine, S: 1997, Kronos: A verification tool for real-time systems, International Journal of Software Tools for Technology Transfer 1: 123–133.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Jonker, C.M., Treur, J., Wijngaards, W.C.A. (2002). Requirements Specification and Automated Evaluation of Dynamic Properties of a Component-Based Design. In: Gero, J.S. (eds) Artificial Intelligence in Design ’02. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0795-4_26
Download citation
DOI: https://doi.org/10.1007/978-94-017-0795-4_26
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-6059-4
Online ISBN: 978-94-017-0795-4
eBook Packages: Springer Book Archive