Helping End-User Programmers “Engineer” Dependable Software

Not long ago, most software was written by professional programmers, who could be presumed to have an interest in software engineering methodologies and in tools and techniques for improving software dependability. Today, however, a great deal of software is written not by professionals but by end-users, who create applications such as multimedia simulations, dynamic web pages, and spreadsheets. Applications such as these are often used to guide important decisions or aid in important tasks, and it is important that they be sufficiently dependable, but evidence shows that they frequently are not. For example, studies have shown that a large percentage of the spreadsheets created by end-users contain faults, and stories abound of spreadsheet faults that have led to multi-million dollar losses. Despite such evidence, until recently, relatively little research had been done to help end-users create more dependable software.

Using Source-Code Analysis to Help End-user Programmers Create Dependable Software

Not long ago, most software was written by professional programmers, who could be presumed to have an interest in software engineering methodologies and in tools and techniques for improving software dependability. Today, however, a great deal of software is written not by professionals but by end-users, who create applications such as multimedia simulations, dynamic web pages, and spreadsheets. Applications such as these are often used to guide important decisions or aid in important tasks, and it is important that they be sufficiently dependable, but evidence shows that they frequently are not. For example, studies have shown that a large percentage of the spreadsheets created by end-users contain faults. Despite such evidence, until recently, relatively little research had been done to help end-users create more dependable software. We have been working to address this problem by finding ways to provide at least some of the benefits of formal software engineering techniques to end-user programmers. In this talk, focusing on the spreadsheet application paradigm, I present several of our approaches, focusing on methodologies that utilize source-code-analysis techniques to help end-users build more dependable spreadsheets. Behind the scenes, our methodologies use static analyses such as dataflow analysis and slicing, together with dynamic analyses such as execution monitoring, to support user tasks such as validation and fault localization. I show how, to accommodate the user base of spreadsheet languages, an interface to these methodologies can be provided in a manner that does not require an understanding of the theory behind the analyses, yet supports the interactive, incremental process by which spreadsheets are created. Finally, I present empirical results gathered in the use of our methodologies that highlight several costs and benefits trade-offs, and many opportunities for future work.

Next Generation Catalogs (NGCs) : Meeting User Needs with Metadata and Search Technology

Recommendations • Become a beta partner with vendor • Test load collections before going live • Update cataloging codes to benefit your community • Don’t expect to drastically change cataloging practices

Towards a Model of Information Systems User Competency

The ability to utilize information systems (IS) effectively is becoming a necessity for business professionals. However, individuals differ in their abilities to use IS effectively, with some achieving exceptional performance in IS use and others being unable to do so. Therefore, developing a set of skills and attributes to achieve IS user competency, or the ability to realize the fullest potential and the greatest performance from IS use, is important. Various constructs have been identified in the literature to describe IS users with regard to their intentions to use IS and their frequency of IS usage, but studies to describe the relevant characteristics associated with highly competent IS users, or those who have achieved IS user competency, are lacking. This research develops a model of IS user competency by using the Repertory Grid Technique to identify a broad set of characteristics of highly competent IS users. A qualitative analysis was carried out to identify categories and sub-categories of these characteristics. Then, based on the findings, a subset of the model of IS user competency focusing on the IS-specific factors – domain knowledge of and skills in IS, willingness to try and to explore IS, and perception of IS value – was developed and validated using the survey approach. The survey findings suggest that all three factors are relevant and important to IS user competency, with willingness to try and to explore IS being the most significant factor. This research generates a rich set of factors explaining IS user competency, such as perception of IS value. The results not only highlight characteristics that can be fostered in IS users to improve their performance with IS use, but also present research opportunities for IS training and potential hiring criteria for IS users in organizations.

Analysis and Transformation of Pipe-like Web Mashups for End User Programmers

Mashups are becoming increasingly popular as end users are able to easily access, manipulate, and compose data from several web sources. To support end users, communities are forming around mashup development environments that facilitate sharing code and knowledge. We have observed, however, that end user mashups tend to suffer from several deficiencies, such as inoperable components or references to invalid data sources, and that those deficiencies are often propagated through the rampant reuse in these end user communities. In this work, we identify and specify ten code smells indicative of deficiencies we observed in a sample of 8,051 pipe-like web mashups developed by thousands of end users in the popular Yahoo! Pipes environment. We show through an empirical study that end users generally prefer pipes that lack those smells, and then present eleven specialized refactorings that we designed to target and remove the smells. Our refactorings reduce the complexity of pipes, increase their abstraction, update broken sources of data and dated components, and standardize pipes to fit the community development patterns. Our assessment on the sample of mashups shows that smells are present in 81% of the pipes, and that the proposed refactorings can reduce that number to 16%, illustrating the potential of refactoring to support thousands of end users developing pipe-like mashups.

Parental Ethnotheories of Child Development: Looking Beyond Independence and Individualism in American Belief Systems

Over the past several decades, the topic of child development in a cultural context has received a great deal of theoretical and empirical investigation. Investigators from the fields of indigenous and cultural psychology have argued that childhood is socially and historically constructed, rather than a universal process with a standard sequence of developmental stages or descriptions. As a result, many psychologists have become doubtful that any stage theory of cognitive or socialemotional development can be found to be valid for all times and places. In placing more theoretical emphasis on contextual processes, they define culture as a complex system of common symbolic action patterns (or scripts) built up through everyday human social interaction by means of which individuals create common meanings and in terms of which they organize experience. Researchers understand culture to be organized and coherent, but not homogenous or static, and realize that the complex dynamic system of culture constantly undergoes transformation as participants (adults and children) negotiate and re-negotiate meanings through social interaction. These negotiations and transactions give rise to unceasing heterogeneity and variability in how different individuals and groups of individuals interpret values and meanings. However, while many psychologists—both inside and outside the fields of indigenous and cultural psychology–are now willing to give up the idea of a universal path of child development and a universal story of parenting, they have not necessarily foreclosed on the possibility of discovering and describing some universal processes that underlie socialization and development-in-context. The roots of such universalities would lie in the biological aspects of child development, in the evolutionary processes of adaptation, and in the unique symbolic and problem-solving capacities of the human organism as a culture-bearing species. For instance, according to functionalist psychological anthropologists, shared (cultural) processes surround the developing child and promote in the long view the survival of families and groups if they are to demonstrate continuity in the face of ecological change and resource competition, (e.g. Edwards & Whiting, 2004; Gallimore, Goldenberg, & Weisner, 1993; LeVine, Dixon, LeVine, Richman, Leiderman, Keefer, & Brazelton, 1994; LeVine, Miller, & West, 1988; Weisner, 1996, 2002; Whiting & Edwards, 1988; Whiting & Whiting, 1980). As LeVine and colleagues (1994) state: A population tends to share an environment, symbol systems for encoding it, and organizations and codes of conduct for adapting to it (emphasis added). It is through the enactment of these population-specific codes of conduct in locally organized practices that human adaptation occurs. Human adaptation, in other words, is largely attributable to the operation of specific social organizations (e.g. families, communities, empires) following culturally prescribed scripts (normative models) in subsistence, reproduction, and other domains [communication and social regulation]. (p. 12) It follows, then, that in seeking to understand child development in a cultural context, psychologists need to support collaborative and interdisciplinary developmental science that crosses international borders. Such research can advance cross-cultural psychology, cultural psychology, and indigenous psychology, understood as three sub-disciplines composed of scientists who frequently communicate and debate with one another and mutually inform one another’s research programs. For example, to turn to parental belief systems, the particular topic of this chapter, it is clear that collaborative international studies are needed to support the goal of crosscultural psychologists for findings that go beyond simply describing cultural differences in parental beliefs. Comparative researchers need to shed light on whether parental beliefs are (or are not) systematically related to differences in child outcomes; and they need meta-analyses and reviews to explore between- and within-culture variations in parental beliefs, with a focus on issues of social change (Saraswathi, 2000). Likewise, collaborative research programs can foster the goals of indigenous psychology and cultural psychology and lay out valid descriptions of individual development in their particular cultural contexts and the processes, principles, and critical concepts needed for defining, analyzing, and predicting outcomes of child development-in-context. The project described in this chapter is based on an approach that integrates elements of comparative methodology to serve the aim of describing particular scenarios of child development in unique contexts. The research team of cultural insiders and outsiders allows for a look at American belief systems based on a dialogue of multiple perspectives.

Psychology and psychoanalysis in Brazil - From cultural syncretism to the collapse of liberal individualism

This paper focuses first on cultural syncretism, used to characterize Brazilian culture. The other aspect of this socially and racially blended culture is the unfinished assimilation of liberalism in politics and the economy, which defines Brazilian society. The increased assimilation and dissemination of psychology may be linked with these in cultural and social aspects. During the military period (1964-1974) the major expansion in university-level studies in psychology contributed ideologically to the dissemination of psychology throughout Brazilian society. This introduced a type of psychology that was related primarily to clinical practice and developed in opposition to social work practice. This paper examines the ideological bases for this conflict between clinical and social work. Criteria for understanding the cultural dissemination of psychoanalysis are then discussed, and it is argued that cultural incorporation of psychoanalysis involves the development of discourse complexes to reflect particular aspects of Brazilian society. The criteria (a non-totalitarian society and the displacement of a magical and religious interpretation of mental disturbance by psychiatric interpretation) are evaluated in relation to the peculiarities of Brazilian syncretism. The paper argues that cultural syncretism and the incomplete assimilation of liberal ideology must be included as criteria in understanding the particular cultural incorporation of psychoanalysis in Brazil.

Riverbed: A Novel User-Steered Image Segmentation Method Based on Optimum Boundary Tracking

This paper presents an optimum user-steered boundary tracking approach for image segmentation, which simulates the behavior of water flowing through a riverbed. The riverbed approach was devised using the image foresting transform with a never-exploited connectivity function. We analyze its properties in the derived image graphs and discuss its theoretical relation with other popular methods such as live wire and graph cuts. Several experiments show that riverbed can significantly reduce the number of user interactions (anchor points), as compared to live wire for objects with complex shapes. This paper also includes a discussion about how to combine different methods in order to take advantage of their complementary strengths.

Comparison of multiple-input single-output single-user ultra-wideband systems with pre-distortion

This paper presents a performance analysis of a baseband multiple-input single-output ultra-wideband system over scenarios CM1 and CM3 of the IEEE 802.15.3a channel model, incorporating four different schemes of pre-distortion: time reversal, zero-forcing pre-equaliser, constrained least squares pre-equaliser, and minimum mean square error pre-equaliser. For the third case, a simple solution based on the steepest-descent (gradient) algorithm is adopted and compared with theoretical results. The channel estimations at the transmitter are assumed to be truncated and noisy. Results show that the constrained least squares algorithm has a good trade-off between intersymbol interference reduction and signal-to-noise ratio preservation, providing a performance comparable to the minimum mean square error method but with lower computational complexity. Copyright (C) 2011 John Wiley & Sons, Ltd.

Towards a hybrid approach for adapting web graphical user interfaces to heterogeneous devices using context

Ubiquitous Computing promises seamless access to a wide range of applications and Internet based services from anywhere, at anytime, and using any device. In this scenario, new challenges for the practice of software development arise: Applications and services must keep a coherent behavior, a proper appearance, and must adapt to a plenty of contextual usage requirements and hardware aspects. Especially, due to its interactive nature, the interface content of Web applications must adapt to a large diversity of devices and contexts. In order to overcome such obstacles, this work introduces an innovative methodology for content adaptation of Web 2.0 interfaces. The basis of our work is to combine static adaption - the implementation of static Web interfaces; and dynamic adaptation - the alteration, during execution time, of static interfaces so as for adapting to different contexts of use. In hybrid fashion, our methodology benefits from the advantages of both adaptation strategies - static and dynamic. In this line, we designed and implemented UbiCon, a framework over which we tested our concepts through a case study and through a development experiment. Our results show that the hybrid methodology over UbiCon leads to broader and more accessible interfaces, and to faster and less costly software development. We believe that the UbiCon hybrid methodology can foster more efficient and accurate interface engineering in the industry and in the academy.

GEDI: a user-friendly toolbox for analysis of large-scale gene expression data

Abstract Background Several mathematical and statistical methods have been proposed in the last few years to analyze microarray data. Most of those methods involve complicated formulas, and software implementations that require advanced computer programming skills. Researchers from other areas may experience difficulties when they attempting to use those methods in their research. Here we present an user-friendly toolbox which allows large-scale gene expression analysis to be carried out by biomedical researchers with limited programming skills. Results Here, we introduce an user-friendly toolbox called GEDI (Gene Expression Data Interpreter), an extensible, open-source, and freely-available tool that we believe will be useful to a wide range of laboratories, and to researchers with no background in Mathematics and Computer Science, allowing them to analyze their own data by applying both classical and advanced approaches developed and recently published by Fujita et al. Conclusion GEDI is an integrated user-friendly viewer that combines the state of the art SVR, DVAR and SVAR algorithms, previously developed by us. It facilitates the application of SVR, DVAR and SVAR, further than the mathematical formulas present in the corresponding publications, and allows one to better understand the results by means of available visualizations. Both running the statistical methods and visualizing the results are carried out within the graphical user interface, rendering these algorithms accessible to the broad community of researchers in Molecular Biology.

Accessibility and demand at an Emergency Care Unit: the user's perspective

AIM: To analyze the search for Emergency Care (EC) in the Western Health District of Ribeirão Preto (São Paulo), in order to identify the reasons why users turn to these services in situations that are not characterized as urgencies and emergencies. METHODS: A qualitative and descriptive study was undertaken. A guiding script was applied to 23 EC users, addressing questions related to health service accessibility and welcoming, problem solving, reason to visit the EC and care comprehensiveness. RESULTS: The subjects reported that, at the Primary Health Care services, receiving care and scheduling consultations took a long time and that the opening hours of these services coincide with their work hours. At the EC service, access to technologies and medicines was easier. CONCLUSION: Primary health care services have been unable to turn into the entry door to the health system, being replaced by emergency services, putting a significant strain on these services' capacity.

PRoSPer: perceptual similarity queries in medical CBIR systems through user profiles

In this paper, we present a novel approach to perform similarity queries over medical images, maintaining the semantics of a given query posted by the user. Content-based image retrieval systems relying on relevance feedback techniques usually request the users to label relevant/irrelevant images. Thus, we present a highly effective strategy to survey user profiles, taking advantage of such labeling to implicitly gather the user perceptual similarity. The profiles maintain the settings desired for each user, allowing tuning of the similarity assessment, which encompasses the dynamic change of the distance function employed through an interactive process. Experiments on medical images show that the method is effective and can improve the decision making process during analysis.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.