Usability and accessibility have become increasingly important in computing curricula. This article briefly reviews how these concepts may be included in existing courses. The authors conducted a survey of student attitudes toward these issues at the start and end of a usability engineering course that included a group project with an accessibility component. Results of the survey indicate that students’ awareness of issues related to usability and accessibility are increased after taking the course and completing the project. Our work and results are potentially valuable to CS educators in three ways: (1) They validate the usefulness of the survey instrument in assessing pedagogies in usability engineering, (2) They provide useful insights into the attitudes of CS majors relative to the important topics of usability and accessibility, and (3) They point to possible benefits of including usability and accessibility topics into CS curricula.

Some of the most challenging tasks in building a software system are capturing, refining, and analyzing requirements. How well these tasks are performed significantly impacts the quality of the developed software system. The difficulty of these tasks is greatly exacerbated for the software of embedded systems as these systems are commonly used for critical applications, have to operate reliably for long periods of time, and usually have a high degree of complexity. Current embedded systems software development practice, however, often deals with the (requirements) analysis phase in a superficial manner, instead emphasizing design and implementation. This research investigates how an approach similar to the well-known design patterns, termed object analysis patterns, can be applied in the analysis phase of embedded systems development, prior to design and coding. Specifically, our research explores how object-oriented modeling notations, such as the Unified Modeling Language (UML), can be used to represent structural and behavioral information as part of commonly occurring object analysis patterns. This work also investigates how UML-based conceptual models of embedded systems, based on the diagram templates in the object analysis patterns, can be automatically analyzed using the Spin model checker for adherence to properties specified in linear-time temporal logic (LTL) using a previously developed UML formalization framework. We have applied these patterns to several embedded systems applications obtained from the automotive industry. This paper describes one of our case studies and illustrates how our approach facilitates the construction of UML-based conceptual models of embedded systems and the analysis of these models for adherence to functional requirements.

This project complements and extends previous work that has focused on attaching formal semantics to informal graphical object-oriented modeling notations in order to automatically generate formal specifications for a number of target languages (Bourdeau and Cheng, 1995; Wang et al., 1997). My research (Campbell and Cheng, 2000; Campbell et al., 2000; Cheng et al., 2000) builds upon the informal and formal integration work by investigating how commonly used automated analysis techniques, such as simulators, model checkers, rewriting systems, and theorem provers can be combined and used in tandem. The main artifacts that are being analyzed are the formal specifications generated from the informal diagrams. The automated analysis enables a developer to check the system design for various properties, such as freedom from deadlock or constraint satisfaction (i.e, specific conditions are satisfied). The formal semantics for the diagrams also makes it possible to execute the graphical models, via the formal specifications, in order to validate the behavior of the system design.

The Unified Modeling Language (UML) comprises several different notations for object-oriented modeling with no formal semantics attached to the individual diagrams. We have developed a generic framework for formalizing a subset of UML diagrams in terms of various formal languages, with a focus on embedded systems. We have formalized UML in terms of Promela, thus enabling analysis of the UML diagrams by the SPIN model checker and simulator. We have also developed a number of visualizations to assist in the interpretation of the analysis results. This paper presents a case study of the UML design and automated analysis of an industrial automotive embedded system using our formalization techniques, supporting tools and existing analysis.

As the impact of and demand for software increases, there is greater need for rigorous software development techniques that can be used by a typical software engineer. In order to integrate informal and formal approaches to software development, we added formal syntax and semantics definitions to existing object-oriented modeling notations. This formalization enables developers to construct object-oriented models of requirements and designs and then automatically generate formal specifications for the diagrams. This paper describes how the resulting diagrams via their specifications can be analyzed using automated techniques to validate behavior through simulation or to check for numerous properties of the diagrams, including inter- and intramodel consistency.