3,458 papers · page 131 of 173
We propose a modular verification methodology for aspect oriented programs. Aspects are the new modularization units to encapsulate crosscutting concerns and have powerful features whose effects can drastically change software behavior. Having such an impact on behavior requires …
When a system fails to meet its specification, it can be difficult to find the source of the error and determine how to fix it. In this paper, we introduce error reporting logic (ERL), an algorithm and tool that produces succinct explanations for why a target system violates a sp…
Maintaining traceability links among software artifacts is particularly important for many software engineering tasks. Even though automatic traceability link recovery tools are successful in identifying the semantic connections among software artifacts produced during software d…
My first attempt to build a "formal development support system" was in IBM in the 1970s; more public is the mural system we built in Manchester; the Rodin (EU) project developed a set of open source tools that are now being used in the (EU) DEPLOY project. These attempts give me …
Unit tests are focused, efficient, and there are many techniques to support their automatic generation. Coarser granularity tests, however, are necessary to validate the behavior of larger software components, and are also likely to be more robust in the presence of program chang…
Writing correct multithreaded programs is difficult. Existing tools for finding bugs in multithreaded programs primarily focus on finding generic concurrency problems such as data races, atomicity violations, and deadlocks. However, these generic bugs may sometimes be benign and …
A software product line (SPL) is an efficient means to generate a family of program variants for a domain from a single code base. However, because of the potentially high number of possible program variants, it is difficult to test all variants and ensure properties like type-sa…
We present a novel approach for black-box testing of database management systems (DBMS) using the Alloy tool-set. Given a database schema and an SQL query as inputs, our approach first formulates Alloy models for both inputs, and then using the Alloy Analyzer, it generates (1) in…
Personal health care applications on mobile devices allow patients to enhance their health via reminders, monitoring and feedback to health care providers. Engineering such applications is challenging with a need for health care plan meta-models, per-patient instantiation of care…
Flash memory has become virtually indispensable in most mobile devices. In order for mobile devices to operate successfully, it is essential that the flash memory be controlled correctly through the device driver software. However, as is typical for embedded software, conventiona…
When a software product is composed of dozens of or even hundreds of components with complicated dependency relationship among each other, one component's change can affect lots of other components' behavior. Sometimes, therefore, the stabilization job with multiple updated compo…
In this paper we use formal software engineering techniques to support one of the most difficult steps in software engineering: learning to use a programming language. In order to support numerous exercises of a large number of students some automatic support for checking the sol…
MaramaEML is an integrated support tool for the enterprise modelling language (EML) built using the Eclipse based Marama framework. It provides support for multiple visual notations including: the business process modelling notation (BPMN); the EML tree- based, multi-layer hierar…
We present and investigate the problem of mining scenario-based triggers and effects from execution traces, in the framework of Damm and Harel's live sequence charts (LSC); a visual, modal, scenario-based, inter-object language. Given a 'trigger scenario', we extract LSCs whose p…
We present the results of a controlled experiment aiming at analysing the role played by the approach adopted during an IR-based traceability recovery process. In particular, we compare the tracing performances achieved by subjects using the "one-shot" process, where the full ran…
For anything but the simplest of software systems, the ease and costs associated with change management can become critical to the success of a project. Establishing traceability initially can demand questionable effort, but sustaining this traceability as changes occur can be a …
Nowadays different notations for architectural modeling have been proposed, each one focussing on a specific application domain, analysis type, or modeling environment. No effective interoperability is possible to date. DUALLY is an automated framework that aims to offer an answe…
In this paper, we present a two-step approach for modelling controlled flexibility in software processes: (1) senior process engineers express which, where and how changes can be applied onto process elements, (2) other process participants can easily identify which changes they …
Developing model-based automatic debugging strategies has been an active research area for several years, with the aim of locating defects in a program by utilising fully automated generation of a model of the program from its source code. We provide an overview of current techni…
Recent developments in runtime verification and monitoring show that parametric regular and temporal logic specifications can be efficiently monitored against large programs. However, these logics reduce to ordinary finite automata, limiting their expressivity. For example, neith…