Alloy is a little language for describing structural properties. It offers a declaration syntax compatible with graphical object models, and a set-based formula syntax powerful enough to express complex constraints and yet amenable to a fully automatic semantic analysis. Its meaning is given by translation to an even smaller (formally defined) kernel. To make Alloy easy to use, a number of complications have been avoided: there are no tuples, no set or relation constants, and no undefined expressions or special null values. This paper presents the language in its entirety, and explains its motivation, contributions and deficiencies.
Acme is a simple, generic software architecture description language (ADL) that can be used as a common interchange format for architecture design tools and/or as a foundation for developing new architectural design and analysis tools. This site provides an introduction to Acme along with a collection of useful Acme software and technical information.
Cqual is a type-based analysis tool that provides
a lightweight, practical mechanism for specifying and checking properties of C
programs. Cqual extends the type system of C with
extra user-defined type qualifiers. The programmer adds type qualifier
annotations to their program in a few key places, and Cqual
performs qualifier inference to check whether the annotations are
correct. The analysis results are presented with a user interface that lets the
programmer browse the inferred qualifiers and their flow paths.whether the annotations are correct. The analysis results are presented with a user interface that lets the programmer browse the inferred qualifiers and their flow paths.
Builds on the notion of safety cases, i.e., structured argumentation to show that safety properties hold for a system. The specific approach being evaluated for HDCP uses a graphical notation to display the structure of an argument concisely. The notation also can provide cross-references to detailed supporting data and information, and has potential for identifying the potential implications of a change to a system.
Hackystat is an experimental testbed for personal metrics validation. It is our third generation of research on empirically guided software process improvement. In the first generation, we investigated the Personal Software Process (PSP), which was introduced by the SEI at CMU in 1995 and involved manual, aper-based collection of developer process data (such as time, size, and defects). PSP has demonstrated some striking benefits: users can often improve their software size and time estimation accuracy to around 90% or better. However, PSP is complicated to learn and the overhead of manual data collection and analysis may be prohibitive. Furthermore, as art of our research on PSP, we did an empirical study of PSP data quality that showed that the method may suffer from significant data quality problems.
Mae is a modeling environment that enables the architect to store and track architectural artifacts, select a particular subset of these artifacts, and analyze the properties of a thus selected architecture. The tool also provides utilities to manage the evolution of artifacts by storing different versions and variants of the elements and tracking the changes from one version to the other.
Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.
The NetFT project is exploring novel fault tolerance techniques for microprocessor-based network interfaces. The key idea behind the project is that the presence of a network processor in the node of a distributed system provides new avenues for network-level and network-assisted fault tolerance. Compute resources available on the network interface help to incorporate fault tolerance in a minimally intrusive manner to the nodes/application. The synergetic and mutually assistive use of compute resources in the network interfaces lead to a networked system with a fault tolerance level that is far greater than what can be achieved with an implementation that confines fault tolerance mechanisms within the host system.
Developer: Dennis Dams, Patrice Godefroid, Kedar Namjoshi
Orion is a tool for statically analyzing C and C++ code for programming errors. The tool works at compile-time, and targets common errors such as failure to initialize a variable, dereferencing an uninitialized pointer, and out-of-bounds array indexing. These types of errors are insidious, in that they often manifest themselves at program points far removed from the source of the problem, and it is extremely difficult to trace them back to the source.
One of the major efforts in Orion is to reduce the false error report ratio to 20% or less. This is achieved by a combination of front-end model checking algorithms that produce relatively few false errors and back-end symbolic analysis methods that filter out most of the remaining non-errors.
Another key strength of Orion is its modular design, which allows us to quickly customize its analysis to particular needs. We hope to hear from people interested in trying out the tool, and in working with us to improve its capabilities.
Our technology is intended to find many errors in concurrent programs quickly and automatically. It is therefore a push-button technique, which, in or experience, is what developers like. The drawback of out technique is that, unlike traditional formal methods where ALL errors are potentially found, we may miss errors (false negatives) and may report non-existent errors (false positives). Therefore, we see it as a tool-at-hand that developers, designers and testers can use with low or no effort, similarly to using a compiler. Combined with some coverage analysis, it can increase reliability and confidence in correctness, due to many errors that have been removed. Combined with a guidance mechanism can influence an operating program to avoid erroneous behaviors when predicted.
The common way to solve state estimation problems is to use Kalman filters. A Kalman filter is essentially a set of mathematical equations implementing a predictor-corrector type estimation that is optimal in the sense that it minimizes the estimated error between the real and the predicted states. Despite their apparent simplicity, implementations of state estimation problems are quite hard to prove correct. Correctness in this context means that the state calculated by a given implementation, called the state estimate, is mathematically optimal when one considers all the hypotheses given in the description of the state estimation problem. Description of such problems are given as sets of stochastic difference equations, and optimality is rigorously, and statistically formulated using matrix differentiation.
In this paper, we present an approach to improving the usability of software systems by means of software architectural decisions. We identify specific connections between aspects of usability, such as the ability to "undo," and software architecture. We also formulate each aspect of usability as a scenario with a characteristic stimulus and response. For every scenario, we provide an architecture pattern that implements its aspect of usability. We then organize the usability scenarios by category. One category presents the benefits of these aspects of usability to users or their organizations. A second category presents the architecture mechanisms that directly relate to the aspects of usability. Finally, we present a matrix that correlates these two categories with the general scenarios that apply to them.
