“What is an algorithm?” is a fundamental question of computer science. Gurevich’s behavioural theory of sequential algorithms (aka the sequential ASM thesis) gives a partial answer by defining (non-deterministic) sequential algorithms axiomatically, without referring to a particular machine model or programming language, and showing that they are captured by (nondeterministic) sequential Abstract State Machines (nd-seq ASMs). However, recursive algorithms such as mergesort are not covered by this theory, as has been pointed out by Moschovakis, who had independently developed a different framework to mathematically characterize the concept of (in particular recursive) algorithm. In this article we propose an axiomatic definition of the notion of sequential recursive algorithm which extends Gurevich’s axioms for sequential algorithms by a Recursion Postulate and allows us to prove that sequential recursive algorithms are captured by recursive Abstract State Machines, an extension of nd-seq ASMs by a CALL rule. Applying this recursive ASM thesis yields a characterization of sequential recursive algorithms as finitely composed concurrent algorithms all of whose concurrent runs are partial-order runs.

Abstract Business process management (BPM) provides many benefits for a company including productivity, efficiency, compliance, risk management, consistency, repeatability, and measurability. Many of these aspects also ensure and improve functional safety, privacy, and security in process execution. However, managed business processes lack flexibility; ie, changing a business process requires more effort than ad hoc execution and adaptation. Thus, especially in small companies, the acceptance rate of managed business processes is low. So we claim that in current BPM approaches, the structuredness ensuring functional safety and security concepts contradicts with the objective for flexibility. The main goal of the AdaBPM project is to address this contradiction by providing a formal approach to handle advanced adaptations and exception handling in business processes. The technical objectives of the project include (1) the definition of a basic framework being capable of handling different levels of adaptivity and considering security and safety requirements at the same time, (2) a rigorous process specification language and model refinement methods, (3) static business process adaptations, and (4) dynamic (or ad hoc) adaptations. The result of our research is a general approach for flexible BPM combined with the possibility to nevertheless manage the process and define safety and security restrictions.

Systems Engineering concerns the complete process for the development of complex systems comprising hardware, software, facilities and personnel. Such systems are hybrid, as some components are characterised by continuous behaviour, whereas the behaviour of others is discrete. SysML provides graphical notations capturing requirements for systems engineering. Here we present a concise conceptual model for systems engineering that is capable to capture the gist of SysML. The structural part is based on the common higher-order Entity Relationship model that is extended by continuous functions and various flow constraints. The behavioural part is then formalised by a hybrid extension of Abstract State Machines. The usage of the conceptual model is illustrated by a working example concerning the landing gear equipment of a plane.

A concurrent Abstract State Machine (ASM) is a family of agents each equipped with a sequential ASM to execute. We define the semantics of concurrent ASMs by concurrent ASM runs which overcome the problems of Gurevich’s distributed ASM runs and generalize Lamport’s sequentially consistent runs. A postulate characterizing an intuitive understanding of concurrency is formulated. It allows us to state and prove an extension of the sequential ASM thesis to a concurrent ASM thesis.

We define a programming language independent controller TaCtl for multi-level transactions and an operator TA, which when applied to concurrent programs with multi-level shared locations containing hierarchically structured complex values, turns their behavior with respect to some abstract termination criterion into a transactional behaviour. We prove the correctness property that concurrent runs under the transaction controller are serialisable, assuming an Inverse Operation Postulate to guarantee recoverability. For its applicability to a wide range of programs we specify the transaction controller TaCtl and the operator TA in terms of Abstract State Machines (ASMs). This allows us to model concurrent updates at different levels of nested locations in a precise yet simple manner, namely in terms of partial ASM updates. It also provides the possibility to use the controller TaCtl and the operator TA as a plug-in when specifying concurrent system components in terms of sequential ASMs.

The geometrically enhanced ER model (GERM) addresses conceptual geometric modelling on two levels. On the surface level GERM is an extended ER model, in which attributes are associated with types with sets of values as domains. On the internal level some of the types, the geometric types, are further associated with geometric domains, which define point sets by means of algebraic curves. For query handling the operations on geometric types give rise to operations on point sets, which can be realized by a small set of operations on algebraic curves. The core problem is then to obtain a surface representation as the result. We show that symbolic computation is essential for solving this problem.

Specification of collaboration has neglected over a long period although collaboration is one of main conceptions in computer science and computer engineering. We distinguish between collaborations among systems and socio-technical collaboration. Database research has succeeded in developing approaches for collaboration among database systems that incorporate conceptual specification and allow to reason on systems at a far higher abstraction level. Conceptual modelling of socio-technical collaborating systems is however an open research issue. With the advent of web information systems systems became naturally socio-technical and collaborating. Therefore, we need a techniques for conceptual description of collaboration. Collaboration modelling may be based on models for communication, models for coordination, and models for cooperation. In socio-technical systems users work within their local environment and collaborate within the global world. Therefore, users inject their culture and their specific behaviour into collaboration. Users use information, communication, cooperation and coordination services. These services must be highly flexible and adaptable to the needs of users, to the circumstances and contexts of these users, and to the technical infrastructures used.

A schema algebra comprises operations on database schemata for a given data model. Such algebras are useful in database design as well as in schema integration. In this article we address the necessary theoretical underpinnings by introducing a novel notion of conceptual schema morphism that captures at the same time the conceptual schema and its semantics by means of the set of valid instances. This leads to a category of schemata that is finitely complete and co-complete. This is the basis for a notion of completeness of schema algebras, if it captures all universal constructions in the category of schemata. We exemplify this notion of completeness for a recently introduced particular schema algebra.

Trust is a critical issue for communication systems. A theory of trust for a given system consists of a set of rules that describe the trust of agents in the system. In a certain logical framework, the theory is generally established based on the security mechanisms of the system. Such a theory provides a foundation for reasoning about agent beliefs as well as security properties that the system may satisfy. For modelling authentication protocols, many researchers have proposed different logical systems. Since communication systems operate in dynamic environments, it is important to model the temporal aspects of such systems in a systematic way. In this paper, we propose a temporalised belief logic called TBL for formalising and verifying authentication protocols.

Partial updates arise when a location bound to a complex value is updated in parallel. Compatibility of such partial updates to disjoint locations can be assured by applying applicative algebras. However, due to the arbitrary nesting of type constructors, locations of complex-value database are often defined at multiple abstraction levels and thereby non-disjoint. Thus, applicative algebras is not as smooth as its simple definition suggests. In this paper, we investigate this problem in the context of complex-value databases, where partial updates arise naturally in database transformations. We show that a more efficient solution can be obtained when generalising the notion of location and thus permitting dependencies between locations. On these grounds we develop a systematic approach to consistency checking for update sets that involve partial updates.

NULL is a special marker used in SQL to indicate that a value for an attribute of an object does not exist in the database. Its aim is a representation of “missing information and inapplicable information”. Although NULL is called null ‘value’ is not at all a value. It is a marker. It is only an annotation of incomplete data. Since it is typically interpreted as a value, NULL has led to controversies and and debates because of its treatment by 3-valued logics, of its special requirements for its use in SQL joins, and the special handling required by aggregate functions and SQL grouping operators.

The emergence of service-oriented computing and cloud computing advocate the development of new software applications on the basis of existing services. To make effectively and efficiently use of existing services, it is essential to describe services so that developers can easily discover and correctly exploit them for their own software development endeavours. In this paper, we present a framework in which existing services available through a cloud are modelled by Abstract State Services. For specification, we use TBox and ABox statements bound to XML Schema and XML. Given such a representation, XQuery can be used for service discovery.

Service-oriented computing, cloud computing, and web services composition mark cornerstones of a paradigm shift in software systems engineering. The general new idea is to use as much as possible services that are made available by others, mostly disseminated via the web. In this paper, we present an abstract model for clouds as federations of services together with a specification of semantics and quality characteristics. For the services as such we adopt the abstract model of abstract state services, which is based on views on some hidden database layer that are equipped with service operations. For the semantics we adopt types for in- and output, pre- and post-conditions, and a description of functionality within an operations ontology. In addition, quality characteristics capture performance, costs, availability, etc. On the basis of this model of clouds, users may conduct a (web) search for usable services, extract service components, and recompose these components. The quality characteristics can be used to optimise the selection of usable services.

In order to increase the expressiveness of XML query languages we define an XML object model that provides a rich description of XML data using the notions of class schema and class tuple. Based on this model we develop a novel query language, the XML Identity Query Language (XIQL) based on identifier generation and fixed-point computation. However, XIQL cannot deal with finite tree duplicates in an XML object graph. To solve this problem we extend XIQL by integrating termsdenoting hereditarily finite sets. With respect to determinate transformations the extended XIQL+is still incomplete, but becomes complete with respect to a modified completeness criterion for XML database transformations, which aims at capturing more non-determinism.

The current transition from Web 1.0 to Web 2.0 is not so much a change of the world wide web itself, but a change of usage. While Web 1.0 is mainly provider-driven, Web 2.0 is user-driven and content-centred. This also implies a fast change of content turning the web from a rather static medium into an active communication medium. Furthermore, the web is subject to even more changes emphasising content, commerce, community and context, personalization, and vertical search, which is branded as the next generation Web 3.0.In this situation the design of Web Information Systems (WISs) requires adaptations to the new developments, if not completely new methods. The tutorial wants to show that the co-design method for WISs did already support many of the features required in Web 2.0 applications. This is particularly stressed by the focus of user contributions to a community or service and the incorporation of collaboration. It will further outline, how the method has to be extended to be fully functional as a Web 2.0 applications development method.The tutorial comprises three parts, the first one dealing with the transition from Web 1.0 to Web 2.0 and beyond, the second one dealing with the co-design methodology with particular emphasis on service orientation, personalisation and contribution to communities, and the final one devoted to the composition of services and collaboration.Part I will give a brief description of three stages that websites have gone through and still will go through: author-driven Web 1.0, user-driven and content-centred Web 2.0, and Web 3.0, which is characterised by (4C+P+VS), where 4C means Content, Commerce, Community and Context, P means Personalization, and VS denotes Vertical Search. In particular, Enterprise 2.0, cloud computing, mashups and Web-Oriented architecture are discussed in detail in order to show the problems in WIS development and the need for WIS development methods. Part II presents the major blocks of our WIS development methodology dealing with strategic modelling of WISs, usage modelling of WISs by means of storyboarding, conceptual modelling of WISs by means of media types, and semantics and pragmatics of storyboarding. Particular attention is paid to services and contributions to communities. Part III focuses on service composition and collaboration showing how the WIS co-design techniques presented in Part II can be adopted to solutions to various Web 2.0 applications including E-Business, Enterprise 2.0, Mashups, thus picking up on the challenges that were highlighted in part I.

Data warehouses integrate and aggregate data from various sources to support decision making within an enterprise. Usually, it is assumed that data are extracted from operational databases used by the enterprise. Web warehousing relaxes this view permitting data sources to be located anywhere on the world-wide web. In this paper we even go one step further and propose that web warehousing should exploit data-intensive web services. For this we adopt the view of the recently introduced model of abstract state services (ASSs). An ASS combines a hidden database layer with an operation-equipped view layer, and can be anything from a simple function to a full-fledged Web Information System, thus provides an abstraction of web services that can be made available for use by other systems, e.g. via the web. We demonstrate how data warehouses and OLAP systems can be considered in a natural way as ASSs, i.e. selected data and functionality of a data warehouse may be made available in the form of a generalised web service, and consequently ASS composition can be used for web warehousing. In order to become workable the model of ASSs has to be extended in a way that allows services to be searched for. For this we propose federations of services together with an ontology that specifies their semantics.

The tutorial will address the various aspects of web information systems (WISs) such as purpose, usage, content, functionality, context, presentation. Starting from the strategic characterisation of a WIS, i.e. the very general question what the WIS is about, we first explore the kind of content that is to be presented in the WIS, and the kind of functionality, with which this content can be accessed, customised to the needs of particular WIS users, and updated. We then explore the modelling of users (or actors) of the WIS, their goals, and the tasks that have to be performed to reach these goals, and general rules for the formation of the WIS presentation.

The exact validation of streaming XML documents can be realised by using visibly push-down automata (VPA) that are defined by Extended Document Type Definitions (EDTD). It is straightforward to represent such an automaton as an Abstract State Machine (ASM). However, creating a whole VPA is not an efficient validation approach. In this paper it is shown, how the VPA construction can be avoided by using a refined ASM that only requires knowledge of the EDTD. In a second step this approach is extended to approximate validation of streaming XML documents taking at most k updates to the document into consideration.

For Web-based e-learning systems personalisation, i.e. the self-adaptation of a system to the preferences and goals of the learners is a highly desirable feature. In this article we start from learner profiles to model preferences and goals. Furthermore, we refine course outlines that are first modelled by directed graphs by Kleene algebras with tests. Then we show how systems can be personalized to different learner profiles simply by reasoning with equations.

Personalization is a hot research topic in Web-based systems. For Web-based electronic learning systems it is an indispensable feature, if we want to provide systems that meet the needs of the learners. In this article, we show how specifications of e-learning systems can be personalized to different learner profiles. For this we describe course outline(s) by directed graphs called outline graphs. Then we discuss several techniques for tailoring the graph according to the needs defined by a learner profile.

Electronic learning systems (ELS) should be contents independent to simplify or enable their reuse with various contents components. Contents independence, however, implies that ELS shouldn't aim at limiting learning space complexity or size. Rather, ELS should aid learners in navigating this space. ELS adaptation to learning style, learner's characteristics and preferences might impact learners accepting these systems. Learners can use the plain look-up function or functions derived from it to trace back to a learning unit.

e-Learning systems will provide new pathways to knowledge and skills acquisition. To increase their quality using a parametric learner model is proposed. Tailoring the learning material presented to the respective parameter values may fit this material to the actual learner's needs. We use a stereotype user model. Our learner characteristics complement the IMS UP. We first represent learners by points in a learner space. Then we propose increasingly generic ways of grouping together such points to form learner types. The less generic one models learner types using convex regions in the learner space. The more generic one models learner types using characteristic functions. While the latter approach allows for more flexible learner type combination the former approach allows for convincing definition of initial learner types. Combining both approaches thus may result in a reasonable number of useful learner types.

Web-based electronic learning systems provide one of the most exciting areas in research with a huge practical impact. However, as these systems are also examples of data-intensive systems, it is astounding how little emphasis is put onto the management of data in these systems. In this article, we present a two-level approach to data modeling in e-learning systems. We suggest modeling a global database level, in which the collection of data of the whole system is modeled in a way that follows the guidelines of good database design. On top of this level we model learning units as extended views. The use of views allows a system modeler to separate course content from underlying database structures. The extension of the learning units by operations models system functionality. Further extensions permit adaptivity to various learner types and end-devices.

Consistency enforcement aims at modifying a program specification such that the result is consistent with respect to a specified set of invariants. Our approach requires the modified program specification to be a maximal consistent diminution of the original one with respect to some partial order. One choice for this partial order is operational specialization, another one arises from the preservation of certain transition invariants. For both choices of the order we obtain a commutativity and a compositionality result which enable a library based pragmatic approach. This sets up a controlled form of automation.

One common usage of the WWW is to provide information services, e.g. for regional event calenders, university lecture management, travel information, etc. Their design requires a clear picture of the system's usage and the supported technical environment. The core of the problem is to provide flexible access units based on extended views on some underlying database. The extension consists of escort information, links, operational facilities and means for the generation of different presentations. We call such units media objects. In order to also allow a flexible presentation for them, we adapt the metaphor of a container. In this way it is possible to present the same information in various ways depending on the user profile and the possible technical restrictions of the display device.