Differences

This shows you the differences between two versions of the page.

Link to this comparison view

blogs:pub2011:compositional_design_and_verification_of_component_based_information_systems [2011/05/09 10:12] (current)
jvogelaar created
Line 1: Line 1:
 +====== Compositional Design and Verification of Component Based Information Systems ======
  
 +J.M.E.M. van der Werf\\
 +//PhD Thesis. Technische Universiteit Eindhoven, Eindhoven, The Netherlands,​ 2011.
 +//
 +
 +===== Abstract =====
 +Information systems have to support more and more complex organizations and the
 +cooperation between organizations. The functionality of these systems is divided in components:
 +each component has its own dedicated set of functionality. Whereas in past
 +years, design and verification mostly focused on the internal aspects of a component,
 +like the data aspect and behavioral aspect, the focus nowadays shifts more and more to
 +the design and verification of the interaction between systems. Different organizations
 +provide systems that need to communicate. Specifically,​ an organization may allow its
 +components to be used by systems of other organizations. This way, an inter organizational
 +network of communicating components is formed. One of the main aspects of such
 +a network is that organizations do not want to share with whom they are communicating.
 +This way, the individual systems form a, possibly unknown, large scale ecosystem: a
 +dynamic network of communicating components. These systems communicate via messages:
 +a component requests a service from another component, which in turn eventually
 +sends its answer. Hence, communication between the components is asynchronous by
 +nature. Verification of asynchronously communicating systems is known to be a hard
 +problem. In this thesis, we develop a framework to design large scale component-based
 +information systems in which components communicate asynchronously. The framework
 +allows for verification of local conditions for termination of the complete system.
 +The formal foundation of the framework is Petri nets, in which communication is
 +asynchronous by nature. Classical Petri nets can be used both for modeling the internal
 +activities of a component, as well as for the interaction between components. We focus on
 +soundness of systems: a system should always have a possibility to terminate. We propose
 +sufficient criteria for compositional verification of soundness: if each component in the
 +system is sound, and each pair of asynchronously communicating components satisfies
 +some condition, the whole system is sound. The framework provides methods to design
 +components that are sound by construction. The method uses soundness preserving
 +refinements of Petri net places in different components by pairs of sound subcomponents.
 +Data can be used to enrich the behavioral aspect, the control flow, of an information
 +system, and data is used to store and present information to the users of the system.
 +Classical Petri nets only focus on the ordering of activities. To integrate the data aspect
 +and behavioral aspect of components, we define a sub class of coloured Petri nets, which
 +is on the one hand expressive enough to model the flow and correlation of objects and
 +messages, and on the other hand the possibility of verification remains.
 +All techniques are combined in a design approach for the development of component
 +based information systems. The approach uses the framework to develop a formal
 +specification from user requirements. The developed specification is directly usable as
 +a prototype, as it has execution semantics. The tool “Yasper” is developed to support
 +the approach. Process mining techniques can be used to support the design process of
 +component based information systems, by extracting internal aspects of a component,
 +like data, resources and control flow. In the thesis, we present a process discovery algorithm
 +based on integer linear programming,​ which can be used for this purpose, as it can
 +handle negative instances that describe undesired behavior.
 +
 +===== Links =====
 +
 +[[http://​www.win.tue.nl/​~jmw/​_media/​public/​proefschrift.pdf| Download PDF]] (3.58 MB)