Search

Software architecture and software architecture practices become increasingly important for information systems since they enable reasoning on the design of the system. The concept of architectural knowledge, i.e. architectural design decisions and the resulting design, plays a pivotal role in architecture. In order to get the most out of architectural knowledge, we need insight into the ways in which architectural knowledge is used. Currently, we lack this insight. We performed survey-based research in the Netherlands to collect feedback on the importance of architectural knowledge for the daily work of practitioners in architecture. We present our findings using two perspectives: the architectural roles practitioners fulfill and the architecture level practitioners are engaged in. We use these perspectives to construct and reflect on the architect's mindset on architectural knowledge. This mindset of architects reveals an approach which is focused on ‘to create and communicate' rather than ‘to review and maintain' an architecture. [ABSTRACT FROM AUTHOR]

Different organizations or organizational units are likely to store and maintain different types of information about their software architectures. This inhibits effective management of architectural knowledge. We experimented with a model of architectural knowledge to characterize the use of architectural knowledge in four different organizations. Based on this experimentation we identified four perspectives on architectural knowledge management, and additionally adjusted the model to better align theory with practice. The refined model defines a minimal set of concepts with supposedly complete coverage of the architectural knowledge domain. Because of the minimalistic aspect of the model, we refer to it as a ‘core model' of architectural knowledge. Supporting evidence for the validity of our model, i.e. the supposed complete coverage, has been obtained by an attempt to falsify this claim through a comparison with selected literature. Application of the core model to characterize the use of architectural knowledge indicates possible areas of improvement for architectural knowledge management in the four organizations. [ABSTRACT FROM AUTHOR]

A large IT company is creating a generic architecting process. Since the company has set an objective to achieve Maturity Level 3 of the Capability Maturity Model Integration (CMMI), the process needs to comply with the relevant requirements set by the CMMI. This paper presents the elicitation of such requirements, and the resulting set of requirements. It analyzes their potential impact on generic architecting processes found in literature. It turns out that many key architectural concepts are at best loosely defined in the CMMI. CMMI is strong in support of the development-related architecting activities, but gives only indirect support for other architecting activities, particularly in a product development context. [ABSTRACT FROM AUTHOR]

Component-based development helps to improve the modularity and reusability of embedded systems. Component models devised for embedded systems are typically restricted due to the limited computing, storage and power resources of the target systems. Most existing component models for embedded systems therefore only support a static component architecture and provide a simple and lightweight core. With the increasing demand for more feature-rich embedded systems these component architectures must be extended. In order to remain useful for the development of resource-restricted embedded systems, however, the extensions must be optional. Creating such extensions requires a cost-effective development process that can produce reusable, rather than application-specific, extensions. This necessitates a systematic approach to seamlessly integrate application specific requirements of the extension, the existing component model and the constraints of the computing environment. In this paper we propose a scenario-based architectural approach to extending the capabilities of the CAmkES component model. This approach is used to distil application specific requirements and computing constraints, summarise generic scenarios, drive the extension to the core CAmkES architecture. We illustrate our approach with a case study involving the addition of dynamic capabilities to CAmkES. [ABSTRACT FROM AUTHOR]

Traceability links are generally recognised as helpful means for improving the effectiveness of evolutionary development processes. However, their practical usage in analysis and design is still unsatisfying, especially due to the high effort required for creation, maintenance and verification of the links, and due to lacking or missing methods and tools for their management. In this paper a concept for the systematic management of traceability is introduced, adapted for the and integrated into the Unified Process as one of the widely accepted software development methods. As an extension, requirements templates are applied to facilitate a tool supported analysis of natural language texts in use case descriptions. Template-based analyses enable a determination of types of terms and a check of their correct application as well as a recognition of implicit connections between development artefacts. A rule set is defined as a first step towards a powerful support of traceability handling. In the ongoing project the rule set is enhanced by heuristics and semantic-based rules to a whole framework of methods and rules. [ABSTRACT FROM AUTHOR]

Self-adaptive systems are capable of changing their behaviour at runtime to meet target constraints. An important research question is how quality of service models can inform runtime adaptation. This paper presents a solution to the problem by application of control theory to improve performance of queued systems by means of architectural adaptation. In a paper presented at the previous year's QoSA conference, we showed how Auto-Regressive Integrated Moving Average techniques can be utilized to forecast how Quality of Service (QoS) characteristics are likely to evolve in the near future. This is particularly important in cases where systems can be adapted to counter QoS constraint violations. In this paper, we show how, given a similar type of QoS characteristic forecasts, strategies of architectural adaptation can be implemented that pre-emptively avoid QoS violations. The novelty of our approach is that we use classical control theory to ensure that our adaptation strategies are stable, in the sense that they do not oscillate between choices. We provide a description of how our control theoretic model can be implemented using context-based interception in .NET via model driven engineering. [ABSTRACT FROM AUTHOR]

Web Services play an important role in the SOA paradigm, as they allow services to be selected on-the-fly to build applications out of existing components. In this scenario, the BPEL notation can be used as an orchestration language which allows the user to describe interactions with Web Services in a standard way. The performance of a BPEL workflow is a very important factor for deciding which components must be selected, or to choose whether a given sequence of interactions can provide the requested quality of service. Due to its very dynamic nature, workflow performance evaluation can not be accomplished using traditional, heavy-weight techniques. In this paper we present a multi-view approach for the performance prediction of service-based applications encompassing both users and service provider(s) perspectives. As a first step towards the realization of this integrated framework we present an efficient approach for performance assessment of Web Service workflows described using the BPEL notation. Starting from annotated BPEL and WSDL specifications, we derive performance bounds on response time and throughput. In such a way users are able to assess the efficiency of a BPEL workflow, while service provider(s) can perform sizing studies or estimate performance gains of alternative upgrades to existing systems. To bring this approach to fruition we developed a prototype tool called bpel2qnbound, using which we analyze a simple case study. [ABSTRACT FROM AUTHOR]

Modern society relies heavily on complex software systems for everyday activities. Dependability of these systems thus has become a critical feature that determines which products are going to be successfully and widely adopted. In this paper, we present an approach to modeling reliability of software systems at the architectural level. Dynamic Bayesian Networks are used to build a stochastic reliability model that relies on standard models of software architecture, and does not require implementation-level artifacts. Reliability values obtained via this approach can aid the architect in evaluating design alternatives. The approach is evaluated using sensitivity and uncertainty analysis. [ABSTRACT FROM AUTHOR]

To support software architecture evaluation practices, several efforts have been made to provide a basis for comparing and assessing evaluation methods, document various best practices, and report the factors that may influence industrial practices. However, there has been no study to explore the experiences and perceptions of architects for determining the factors that influence architecture evaluation practices in a wide range of organizations. Hence, there is little empirically founded knowledge available on the factors that influence the industrial practices of software architecture evaluation. The goal of this paper is to report the results of an empirical study aimed at gaining an understanding of different factors involved in evaluating architectures in industry. The results of this study shed light on the factors that influence architecture evaluation practices based on the experiences and perception of architects who regularly evaluate architectures of various sizes of applications. It also discusses some of the strategies that practitioners apply to deal with the influence of the identified factors. [ABSTRACT FROM AUTHOR]

Performance predictions aim at increasing the quality of software architectures during design time. To enable such predictions, specifications of the performance properties of individual components within the architecture are required. However, the response times of a component might depend on its configuration in a specific setting and the data send to or retrieved from it. Many existing prediction approaches for component-based systems neglect these influences. This paper introduces extensions to a performance specification language for components, the Palladio Component Model, to model these influences. The model enables to predict response times of different architectural alternatives. A case study on a component-based architecture for a web portal validates the approach and shows that it is capable of supporting a design decision in this scenario. [ABSTRACT FROM AUTHOR]

Organizations use to have implemented systems that represent a large effort and budget invested in the past. These systems are evolved and adapted over time in order to accommodate technological and business changes. Moreover, big companies often develop similar systems within the same domain. This has been motivating them to migrate to reuse approaches, such as domain engineering and product line. However, existing systems in general don't have up-to-date architectural documentation that can help in their maintenance and reuse. Considering this scenario, this paper presents an approach to architecture recovery and evaluation that aims at extracting knowledge from existing systems to help in their understanding and reuse. This extracted knowledge is represented through a recovered application architectural model composed by architectural elements that represent domain concepts traced to implemented functional requirements, which may help in generating reusable artifacts. In order to evaluate the approach feasibility, an experimental study was performed. [ABSTRACT FROM AUTHOR]

In enterprise application development and other software construction projects, a critical success factor is to make sound architectural decisions. Text templates and tool support for capturing architectural decisions exist, but have failed to reach broad adoption so far. One of the inhibitors we perceived on large-scale industry projects is that architectural decision capturing is regarded as a retrospective and therefore unwelcome documentation task which does not provide any benefit during the original design work. A major problem of such a retrospective approach is that the decision rationale is not available to decision makers when they identify, make, and enforce decisions. Often a large, possibly distributed, community of decision makers is involved in these three steps. In this paper, we propose a new conceptual framework for proactive decision identification, decision maker collaboration, and decision enforcement. Based on a meta model capturing reuse and collaboration aspects explicitly, our framework instantiates decision models from requirements models and re usable decision templates. These templates capture know ledge gained on other projects em ploy ing the same architectural style. As an exemplary application of these concepts to service-oriented architecture shows, reusable architectural decision models can speed up the decision identification and improve the quality of the decision making. Reusable architectural decision models can also simplify the exchange of architecture design rationale within and between project teams, and expose decision out come as model transformation parameters in model-driven software development. [ABSTRACT FROM AUTHOR]

A software architecture design captures the main decisions regarding the quality-attribute requirements for a system. When constructing these designs, the architect normally evaluates and combines solutions with different quality-attribute tradeoffs. This exploration of the design space can be seen as a searching problem, in which the architect's expertise is what directs the search towards a "good-enough" solution. Nonetheless, given complexity of this search, assisting the architect with adequate tool support becomes indispensable. In this context, we have investigated the utility of a planning-based tool approach called DesignBots to explore design alternatives. Specifically, the approach considers quality-attribute issues as goals achievable by combinations of architectural mechanisms, which are generated by a mixed-initiative and hierarchical planning engine. Our experiences with DesignBots show that the planning approach effectively helps architects to explore design alternatives productively. [ABSTRACT FROM AUTHOR]

The concept of resource architecture has been introduced to describe the association of operations with resources, and interactions between these operations. This paper explains resource architecture with examples, and how it can be used in performance engineering throughout the life of a project. [ABSTRACT FROM AUTHOR]

Pushdown systems (PDSs) consist of a stack and a finite state machine and are frequently used to model abstractions of software. They correspond to sequential recursive programs with finite-domain variables. This paper presents a novel algorithm for deciding reachability of particular locations of PDSs. We exploit the fact that most PDSs used in practice are shallow, and propose to use SAT-based Bounded Model Checking to search for counterexamples. Completeness is achieved by computing universal summaries of the procedures in the program. [ABSTRACT FROM AUTHOR]

This paper presents an approach to the efficient verification of embedded systems. Such systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models, which in turn aggravates the state explosion problem. Careful handling of nondeterminism is therefore crucial for obtaining efficient model checking tools. Here, we support this goal by developing a formal computation model and an abstraction method, called delayed nondeterminism, which instantiates nondeterministic values only if and when this is required by the application code. It is shown how this technique can be integrated into our CTL model checking tool [mc]square by introducing symbolic abstract states which represent several concrete states. We also give a simulation relation between the concrete and the abstract state space, thus establishing the soundness of delayed nondeterminism with respect to "path-universal" logics such as ACTL and LTL. Furthermore, a case study is presented in which three different programs are used to demonstrate the effectiveness of our technique. [ABSTRACT FROM AUTHOR]

Implementations of computer systems comprise many layers and employ a variety of programming languages. Building such systems requires support of an often complex, accompanying tool chain. The Verisoft project deals with the formal pervasive verification of computer systems. Making use of appropriate formal specification and proof tools, this task requires (i) specifying the layers and languages used in the implementation, (ii) specifying and verifying the algorithms employed by the tool chain (or, alternatively, validating their actual output), and (iii) proving simulation statements between layers, arguing about the programs residing at the different layers. Combining the simulation statements for all layers should allow to transfer correctness results for top-layer programs to their bottom-layer representation; in this manner, a verified stack can be built. Maintaining all formal artifacts, the actual system implementation, and the (verification) tool chain is a challenging task. We call sets of tools that help addressing this task system verification environments. In this paper, we describe the structure, contents, and architecture of the system verification environment used in the Verisoft project. [ABSTRACT FROM AUTHOR]

Despite many advances, today's software model checkers and extended static checkers still do not scale well to large code bases, when verifying properties that depend on complex interprocedural flow of data. An obvious approach to improve performance is to exploit software structure. Although a tremendous amount of work has been done on exploiting structure at various levels of granularity, the fine-grained shared structure among multiple verification conditions has been largely ignored. In this paper, we formalize the notion of shared structure among verification conditions, propose a novel and efficient approach to exploit this sharing, and provide experimental results that this approach can significantly improve the performance of verification, even on path- and context-sensitive and dataflow-intensive properties. [ABSTRACT FROM AUTHOR]

Unit testing plays a major role in the software development process. It enables the immediate detection of bugs introduced into a unit whenever code changes occur. Hence, unit tests provide a safety net of regression tests and validation tests which encourage developers to refactor existing code. Nevertheless, not all software systems contain unit tests. When changes to such software are needed, writing unit tests from scratch might not be cost effective. In this paper we propose a technique which automatically generates unit tests for software that does not have such tests. We have implemented GenUTest, a tool which captures and logs inter-object interactions occurring during the execution of Java programs. These interactions are used to generate JUnit tests. They also serve in generating mock aspects - mock object like entities, which assist the testing process. The interactions are captured using the aspect oriented language AspectJ. [ABSTRACT FROM AUTHOR]

Code coverage is often defined as a measure of the degree to which the source code of a program has been tested [19]. Various metrics for measuring code coverage exist. The vast majority of these metrics require instrumenting the source code to produce coverage data. However, for certain coverage metrics, it is also possible to instrument object code to produce coverage data. Traditionally, such instrumentation has been considered inferior to source level instrumentation because source code is the focus of code coverage. Our experience shows that object code instrumentation, specifically post-link instrumentation, can be very useful to users. Moreover, it does not only alleviate certain side-effects of source-level instrumentation, especially those related to compiler optimizations, but also lends itself to performance optimization that enables low-overhead instrumentation. Our experiments show an average of less than 1% overhead for instrumentation at the function level and an average of 4.1% and 0.4% overhead for SPECint2000 and SPECfp2000, respectively, for instrumentation at the basic block level. This paper demonstrates the advantages of post-link coverage and describes effective methodology and technology for applying it. [ABSTRACT FROM AUTHOR]

A regression bug is a bug which causes a feature that worked correctly to stop working after a certain event (system upgrade, system patching, daylight saving time switch, etc.). Very often an encompassed bug fix included in a patch causes the regression bug. Regression bugs are an annoying and painful phenomena in the software development process, requiring a great deal of effort to find. Many tools have been developed in order to find the existence of such bugs. However, a great deal of manual work is still needed to find the exact source-code location that caused a regression bug. In this paper we present the CodePsychologist, a tool which assists the programmer to locate source code segments that caused a given regression bug. The CodePsychologist goes beyond current tools, that identify all the lines of code that changed since the feature in question worked properly (with the help of a Source Control Tool). The CodePsychologist uses various heuristics to select the lines most likely to be the cause of the error, from these often large number of lines of code. This reduces the fixing time of regression bugs. It allows a quick response to field errors that need an immediate correction. [ABSTRACT FROM AUTHOR]

This paper presents dynamic testing, a method that exploits automata learning to systematically test (black box) systems almost without prerequisites. Based on interface descriptions, our method successively explores the system under test (SUT), while it at the same time extrapolates a behavioral model. This is in turn used to steer the further exploration process. Due to the applied learning technique, our method is optimal in the sense that the extrapolated models are most concise in consistently representing all the information gathered during the exploration. Using the LearnLib, our framework for automata learning, our method can elegantly be combined with numerous optimizations of the learning procedure, various choices of model structures, and last but not least, with the option to dynamically/interactively enlarge the alphabet underlying the learning process. All these features will be illustrated using as a case study the web application Mantis, a bug tracking system widely used in practice. We will show how the dynamic testing procedure proceeds and how the behavioral models arise that concisely summarize the current testing effort. It has turned out that these models, besides steering the automatic exploration process, are ideal for user guidance and to support analyzes to improve the system understanding. [ABSTRACT FROM AUTHOR]

Simulation test coverage does not scale gracefully with growing system design size. Component interactions grow exponentially with the number of system components, while conventional system test at best can increase coverage as a linear function of allotted test time. Likewise, capacity limitations are commonly cited as the essential gating factor that restricts the application of automatic formal verification (model checking) to at most a few design blocks. Nonetheless, abstraction has long been used successfully in pilot projects to apply model checking to entire systems. Abstraction in conjunction with guided-random simulation can be used in the same way to increase coverage for conventional test. While academic use of abstraction is old, its use in the EDA industry's commercial tool sets has been very limited, due to a perception that its use entails an unacceptably disruptive methodology change. It is shown here how quite general data-path abstraction incorporated into a hierarchical design flow can be introduced with only a modest change in methodology. This hierarchical design flow supports verification based on either simulation or model checking that can scale gracefully with increasing design complexity. [ABSTRACT FROM AUTHOR]

Reaching hard-to-reach coverage events is a difficult task that requires both time and expertise. Data-driven Coverage Directed Generation (CDG) can assist in the task when the coverage events are part of a structured coverage model, but is a-priori less useful when the target events are singular and not part of a model. We present virtual coverage models as a mean for enabling data-driven CDG to reach singular events. A virtual coverage model is a structured coverage model (e.g., cross-product coverage) defined around the target event, such that the target event is a point in the structured model. With the structured coverage model around the target event, the CDG system can exploit the structure to learn how to reach the target event from covered points in the structured model. A case study of using CDG and virtual coverage to reach a hard-to-reach event in a multi-processor system demonstrates the usefulness of the proposed method. [ABSTRACT FROM AUTHOR]

Software verification is a hard yet important challenge. In general, the problem is undecidable. Nevertheless, it is still beneficial to look at solutions that either restrict the generality or are heuristic in nature (and do not guarantee to terminate). In this paper, we concentrate on a related problem, that of verifying that a cycle in the flow chart of a program does not terminate. We show some exact and sufficient conditions for cycle nontermination, and provide application for program verification. This allows us to check sequential and concurrent programs against temporal properties, using a truly symbolic approach, and to use temporal logic to guide the selection of test cases in such programs. [ABSTRACT FROM AUTHOR]

Constraint Programming (CP) technology has been extensively used in Random Functional Test Generation during the recent years. However, while the existing CP methodologies are well tuned for traditional combinatorial applications e.g. logistics or scheduling, the problem domain of functional test generation remains largely unexplored by the CP community and many of its domain specific features and challenges are still unaddressed. In this paper we focus on the distinctive features of CP for the random functional test generation domain and show how these features can be addressed using a classical CP engine with custom extensions. We present some modeling and solving problems arising in this context and propose solutions. In particular, we address the way of model building in the problem domain of test generation which we refer to as multi-layer modeling. In this context we introduce constraint patterns of composite variable, implied condition and implied composite variable condition, define their semantics and propose schemes for their CSP modeling. The paper also addresses specific problems arising at the solving stage in the problem domain of random test generation. We propose solutions to these problems by means of custom random search algorithms. This approach is illustrated on the examples of the disjunction constraint and conditional variable instantiation. The latter algorithm addresses the feature of dynamic modeling required in the test generation task. To demonstrate the effectiveness of our approach we present experimental results based on the implementation using ILOG Solver as a CP engine. [ABSTRACT FROM AUTHOR]

This paper studies the efficiency of several probabilistic model checkers by comparing verification times and peak memory usage for a set of standard case studies. The study considers the model checkers ETMCC, MRMC, PRISM (sparse and hybrid mode), YMER and VESTA, and focuses on fully probabilistic systems. Several of our experiments show significantly different run times and memory consumptions between the tools—up to various orders of magnitude—without, however, indicating a clearly dominating tool. For statistical model checking YMER clearly prevails whereas for the numerical tools MRMC and PRISM (sparse) are rather close. [ABSTRACT FROM AUTHOR]

The paper presents a new approach to formal verification of generic (i.e. parametrised) hardware designs specified in VHDL. The proposed approach is based on a translation of such designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. We have implemented the proposed translation. Using one of the state-of-the-art tools for verification of counter automata, we were then able to verify several non-trivial properties of parametrised VHDL components, including a real-life one. [ABSTRACT FROM AUTHOR]

Modern hardware designs are typically based on multiple clocks. While a singly-clocked hardware design is easily described in standard temporal logics, describing a multiply-clocked design is cumbersome. Thus, it is desirable to have an easier way to formulate properties related to clocks in a temporal logic. In [6] a relatively simple solution built on top of the traditional ltl semantics was suggested and adopted by the IEEE standard temporal logic psl. The suggested semantics was examined relative to a list of design goals, and it was shown that it answered all requirements except for preserving the least fixed point characterization of the until operator under multiple clocks. In this work we show that with a minor addition to the semantics of [6] this requirement is met as well. [ABSTRACT FROM AUTHOR]

SystemC is a popular language used in modeling system-on-chip implementations. To support this task at a high level of abstraction, transaction-level modeling (TLM) libraries have been recently developped. While TLM libraries are useful, it is difficult to capture the reactive nature of certain transactions with the constructs currently available in the SystemC and TLM libraries. In this paper, we propose an approach to specify and verify reactive transactions in SystemC designs. Reactive transactions are different from TLM transactions in the sense that a transaction can be killed or reset. Our approach consists of: (1) a language to describe reactive transactions that can be translated to verification monitors, (2) an architectural pattern to implement reactive transactions, and (3) the verification support to verify that the design does not deadlock, allows only legal behaviors and is always responsive. We illustrate our approach through an example of a transactional memory system where a transaction can be killed or reset before its completion. We identify the architectural patterns for reactive transactions. Our results demonstrate the feasibility of our approach as well as support for a comprehensive verification using RuleBase/NuSMV tools. [ABSTRACT FROM AUTHOR]

This short paper is the result of the invited talk I gave at the 2007 Haifa Verification Conference. Its purpose is to briefly summarize the main points of my talk and to provide background references. The original talk abstract was, "Dynamic verification (simulation, emulation) and formal verification often live in separate worlds, with minimal interaction between the two camps, yet both have unique strengths that could complement the other. In this talk, I'll briefly enumerate what I believe are the best aspects of each verification style, and then explore some possibilities for drawing on the strengths of both camps." [ABSTRACT FROM AUTHOR]

Parser combinators are higher-order functions used to build parsers as executable specifications of grammars. Some existing implementations are only able to handle limited ambiguity, some have exponential time and/or space complexity for ambiguous input, most cannot accommodate left-recursive grammars. This paper describes combinators, implemented in Haskell, which overcome all of these limitations. [ABSTRACT FROM AUTHOR]

Tabled evaluation has been proved an effective method to improve several aspects of goal-oriented query evaluation, including termination and complexity. Several "native" implementations of tabled evaluation have been developed which offer good performance, but many of them require significant changes to the underlying Prolog implementation, including the compiler and the abstract machine. Approaches based on program transformation, which tend to minimize changes to both the Prolog compiler and the abstract machine, have also been proposed, but they often result in lower efficiency. We explore some techniques aimed at combining the best of these worlds, i.e., developing an extensible implementation which requires minimal modifications to the compiler and the abstract machine, and with reasonably good performance. Our preliminary experiments indicate promising results. [ABSTRACT FROM AUTHOR]

When BDDs are used for propagation in a constraint solver with nogood recording, it is necessary to find a small subset of a given set of variable assignments that is enough for a BDD to imply a new variable assignment. We show that the task of finding such a minimum subset is NP-complete by reduction from the hitting set problem. We present a new algorithm for finding such a minimal subset, which runs in time linear in the size of the BDD representation. In our experiments, the new method is up to ten times faster than the previous method, thereby reducing the solution time by even more than 80%. Due to linear time complexity the new method is able to scale well. [ABSTRACT FROM AUTHOR]

This paper presents an environment to support high-level database programming in the multi-paradigm declarative programming language Curry. We define an application programming interface (API) that abstracts from the concrete database access methods. The API supports transactions and exploits Curry's type system to ensure a strict separation between queries and updates. In order to ensure database updates that are safe w.r.t. an intended data model (e.g., containing specific relations between entities), we assume a description of the data dependencies in the entity-relationship (ER) model from which all access and update operations related to the database are generated. We propose a representation of ER diagrams in the declarative language Curry so that they can be constructed by various tools and then translated into this representation. Furthermore, we have implemented a compiler from this representation into a Curry program that provides safe access and update operations based on the API for database programming. [ABSTRACT FROM AUTHOR]

More and more software systems use a browser as the universal graphical user interface. As a consequence these applications inherit browser navigation as part of their interface. Typical browser actions are the use of the back- and forward-button and the cloning of windows. Browser navigation is difficult to deal with because it has effects that are noticed indirectly by the application logic. It is easy to forget or misunderstand the consequences of this aspect in the construction of a program. Hence, testing the correct behavior of the application is very desirable, preferably with an automatic model-based test tool. For this kind of model-based testing a specification including browser navigation is needed. We introduce a transformation to lift the specification of a program without browser navigation to one with browser navigation. This reduces the specification effort considerably. The distinguishing feature of our method is that it allows the test engineer to specify only the exceptions to the general rule. We show how this lifting of specifications is used for some examples and how errors are found in real web applications. The described system builds on the model-based test tool G∀ST. [ABSTRACT FROM AUTHOR]

In this paper, we present an implementation of a modular synthesizer in Haskell using Yampa. A synthesizer, be it a hardware instrument or a pure software implementation, as here, is said to be modular if it provides sound-generating and sound-shaping components that can be interconnected in arbitrary ways. Yampa, a Haskell-embedded implementation of Functional Reactive Programming, supports flexible, purely declarative construction of hybrid systems. Since music is a hybrid continuous-time and discrete-time phenomenon, Yampa is a good fit for such applications, offering some unique possibilities compared to most languages targeting music or audio applications. Through the presentation of our synthesizer application, we demonstrate this point and provide insight into the Yampa approach to programming reactive, hybrid systems. We develop the synthesizer gradually, starting with fundamental synthesizer components and ending with an application that is capable of rendering a standard MIDI file as audio with respectable performance. [ABSTRACT FROM AUTHOR]

Logtalk, an object oriented logic programming language, provides experimental support for multi-threading programming with selected back-end Prolog compilers. By making use of core, low-level Prolog predicates that interface with operating-system native threads, Logtalk provides a high-level set of directives and predicates that allows programmers to easily take advantage of modern multi-processor and multi-core computers without worrying about the details of creating, synchronizing, or communicating with threads. Logtalk multi-threading programming features include support for concurrent calls akin to and-parallelism and or-parallelism, non-deterministic thread goals, asynchronous calls, and predicate synchronization. The integration with the Logtalk object-oriented features allows objects to send and receive both synchronous and asynchronous messages and to call local predicates concurrently. Logtalk multi-threading features are orthogonal to object-oriented concepts and can be useful even in the context of plain Prolog. [ABSTRACT FROM AUTHOR]

Master-worker systems are a well-known and often applicable scheme for the parallel evaluation of a pool of tasks, a work pool. The system consists of a master process managing a set of worker processes. After an initial phase with a fixed amount of tasks for each worker, further tasks are distributed in reply to results sent back by the workers. As this setup quickly leads to a bottleneck in the master process, the paper investigates techniques for hierarchically nesting the basic master-worker scheme. We present implementations of hierarchical master-worker skeletons, and how to automatically calculate parameters of the nested skeleton for good performance. Nesting master-worker systems is nontrivial especially in cases where new tasks are dynamically created from previous results (typically breadth- or depth-first tree search algorithms). We discuss how to handle dynamically growing pools in a hierarchy and present a declarative implementation for nested master-worker systems with dynamic task creation. The skeletons are experimentally evaluated with two typical test programs. We analyse their runtime behaviour and the effects of different hierarchies on runtimes via trace visualisations. [ABSTRACT FROM AUTHOR]

Most efficient implementations of parallel logic programming rely on complex low-level machinery which is arguably difficult to implement and modify. We explore an alternative approach aimed at taming that complexity by raising core parts of the implementation to the source language level for the particular case of and-parallelism. We handle a significant portion of the parallel implementation at the Prolog level with the help of a comparatively small number of concurrency-related primitives which take care of lower-level tasks such as locking, thread management, stack set management, etc. The approach does not eliminate altogether modifications to the abstract machine, but it does greatly simplify them and it also facilitates experimenting with different alternatives. We show how this approach allows implementing both restricted and unrestricted (i.e., non fork-join) parallelism. Preliminary experiments show that the performance sacrificed is reasonable, although granularity control is required in some cases. Also, we observe that the availability of unrestricted parallelism contributes to better observed speedups. [ABSTRACT FROM AUTHOR]

We present the design and prototype implementation of the scheduling component in ArTCoP(architecture transparent control of parallelism), a novel run-time environment (RTE) for parallel execution of high-level languages. A key feature of ArTCoP is its support for deep process and memory hierarchies, shown in the scheduler by supporting light-weight threads. To realise a system with easily exchangeable components, the system defines a micro-kernel, providing basic infrastructure, such as garbage collection. All complex RTE operations, including the handling of parallelism, are implemented at a separate system level. By choosing Concurrent Haskell as high-level system language, we obtain a prototype in the form of an executable specification that is easier to maintain and more flexible than conventional RTEs. We demonstrate the flexibility of this approach by presenting implementations of a scheduler for light-weight threads in ArTCoP, based on GHC Version 6.6. [ABSTRACT FROM AUTHOR]

Packrat parsing is a newly popular technique for efficiently implementing recursive descent parsers. Packrat parsing avoids the potential exponential costs of recursive descent parsing with backtracking by ensuring that each production rule in the grammar is tested at most once against each position in the input stream. This paper argues that (a) packrat parsers can be trivially implemented using a combination of definite clause grammar rules and memoing, and that (b) packrat parsing may actually be significantly less efficient than plain recursive descent with backtracking, but (c) memoing the recognizers of just one or two nonterminals, selected in accordance with Amdahl's law, can sometimes yield speedups. We present experimental evidence to support these claims. [ABSTRACT FROM AUTHOR]

Domain-specific languages facilitate solving problems in a targeted domain by providing features particular to the domain. Declarative domain-specific languages have the additional benefit that users specify what something means rather than how to do something. As a result, the language compiler is free to choose the best implementation strategies and to generate multiple artifacts from a single description. pads/ml is a declarative data description language designed to facilitate ad hoc data management. From a single description, the compiler generates a myriad of artifacts, including data structures for the in-memory representation of the data and parsers and printers. In this paper, we describe a new generic programming infrastructure for pads/ml that allows third-party developers to define additional useful artifacts without modifying the compiler. We report on two case studies that use this infrastructure. In the first, we build a version of padx for pads/ml, allowing any data source with a pads/ml description to be queried as if it were xml. In the second, we extend Harmony with the ability to synchronize any data with a pads/ml description. [ABSTRACT FROM AUTHOR]

Nonlinear constraint satisfaction or optimisation models need to be reduced to equivalent linear forms before they can be solved by (Integer) Linear Programming solvers. A choice of linearisation methods exist. There are generic linearisations and constraint-specific, user-defined linearisations. Hence a model reformulation system needs to be flexible and open to allow complex and novel linearisations to be specified. In this paper we show how the declarative model reformulation system Cadmium can be used to effectively transform constraint problems to different linearisations, allowing easy exploration of linearisation possibilities. [ABSTRACT FROM AUTHOR]

Pattern matching is a programming language feature for selecting a handler based on the structure of data while binding names to sub-structures. By combining selection and binding, pattern matching facilitates many common tasks such as date normalization, red-black tree manipulation, conversion of XML documents, or decoding TCP/IP packets. Matchete is a language extension to Java that unifies different approaches to pattern matching: regular expressions, structured term patterns, XPath, and bit-level patterns. Matchete naturally allows nesting of these different patterns to form composite patterns. We present the Matchete syntax and describe a prototype implementation. [ABSTRACT FROM AUTHOR]

Declarative authorization languages promise to simplify the administration of access control systems by allowing the authorization policy to be factored out of the implementation of the resource guard. However, writing a correct policy is an error-prone task by itself, and little attention has been given to tools and techniques facilitating the analysis of complex policies, especially in the context of access denials. We propose the use of abduction for policy analysis, for explaining access denials and for automated delegation. We show how a deductive policy evaluation algorithm can be conservatively extended to perform abduction on Datalog-based authorization policies, and present soundness, completeness and termination results. [ABSTRACT FROM AUTHOR]

We address the tension between software generality and performance in the domain of simulations based on Monte-Carlo methods. We simultaneously achieve generality and high performance by a novel development methodology and software architecture centred around the concept of a specialising simulator generator. Our approach combines and extends methods from functional programming, generative programming, partial evaluation, and runtime code generation. We also show how to generate parallelised simulators. We evaluated our approach by implementing a simulator for advanced forms of polymerisation kinetics. We achieved unprecedented performance, making Monte-Carlo methods practically useful in an area that was previously dominated by deterministic PDE solvers. This is of high practical relevance, as Monte-Carlo simulations can provide detailed microscopic information that cannot be obtained with deterministic solvers. [ABSTRACT FROM AUTHOR]

Unification, one of the key processes underlying logic programming (LP), provides a powerful mechanism for assembling and disassembling structures, lists in particular, by matching patterns. In recent work, we showed how spreadsheets can be enhanced by adding a visual form of LP in which lists, the fundamental structures of LP, are replaced by rectangular arrays, the fundamental structures of spreadsheets. The benefits include enhanced programmability and a way to specify high level templates for spreadsheet structures. Here, we focus on the structure of arrays, and describe the array unification algorithm underlying our current implementation. [ABSTRACT FROM AUTHOR]

In this paper we discuss an approach to support declarative reasoning over aspect-oriented (AO) programs, adopting AspectJ as a representative technology. The approach is based on the transformation of source code into a set of facts and rules, stored into a Prolog database. Declarative analysis allows us to extract complex information through its rich and expressive syntax. Our approach has two contributions. First, it aims to improve the comprehension of AspectJ programs. The type of knowledge provided is categorized in three main groups: i) general knowledge, ii) bad smells, and iii) quality metrics. The second contribution is the provision of dependency analysis of AspectJ programs. To that end, we identify dependencies in aspect-oriented programs, and translate them into Prolog rules. Expected beneficiaries of our approach include system maintainers who can obtain comprehension and perform dependency analysis through querying the Prolog database during the change planning stage of system evolution. [ABSTRACT FROM AUTHOR]

An extended practice in the realm of Software Engineering and programming in industry is the application of coding rules. Coding rules are customarily used to constrain the use (or abuse) of certain programming language constructions. However, these rules are usually written using natural language, which is intrinsically ambiguous and which may complicate their use and hinder their automatic enforcement. This paper presents some early work aiming at defining a framework to formalise and check for coding rule conformance using logic programming. We show how a certain class of rules - structural rules - can be reformulated as logic programs, which provides both a framework for formal specification and also for automatic conformance checking using a Prolog engine. Some examples of rules belonging to actual, third-party coding rule sets are discussed, along with the corresponding Prolog code. Experimental data regarding the practicality and impact of their application to real-life software projects is presented and discussed. [ABSTRACT FROM AUTHOR]