Creating and enhancing a software engineering work force requires several different types of continuing education for software professionals, including: task-oriented education, enhancement-oriented education and selection-oriented education. In this paper, we focus on the important, but often neglected, category of selection-oriented education. We begin with a discussion of technology selection, indicating what it involves, how it contributes to improving the state of practice, and why it is key to technology improvement in general. This is followed by a discussion of some criteria for selection-oriented education programs. We then describe the selection-oriented education activities at the Rocky Mountain Institute of Software Engineering and relate some problems encountered in establishing these activities.

An approach to the design of concurrent software systems based on the constrained expression formalism is described. This formalism provides a rigorous conceptual model for the semantics of concurrent computations, thereby supporting analysis of important system properties as part of the design process. This approach allows designers to use standard specification and design languages, rather than forcing them to deal with the formal model explicitly or directly. As a result, the approach attains the benefits of formal rigor without the associated pain of unnatural concepts or notations for its users. The conceptual model of concurrency underlying the constrained expression formalism treats the collection of possible behaviors of a concurrent system as a set of sequences of events. The constrained expression formalism provides a useful closed-form description of these sequences. Algorithms were developed for translating designs expressed in a wide variety of notations into these constrained expression descriptions. A number of powerful analysis techniques that can be applied to these descriptions have also been developed.

We study some consequences of the formal language approach to modelling software system behavior for the case of asynchronous, concurrent subsystems. We use the formal language shuffle operation to give an "algebraic" definition of semantics for a simple (structured) concurrent programming language and prove that the use of this operation is necessary. Having established this necessity, we investigate other types of behavioral expressions which use the operation and show that the analysis problem for these expressions is either undecidable or intractable. The results provide some limitations, for example, on the path expression method of system behavior analysis. Our lower bound proofs involve the use of synchronization symbols, which seem to be a formal language analogue of semaphores.

A modeling scheme is presented which provides a medium for the rigorous, formal, and abstract specification of large-scale software system components. The scheme allows the description of component behavior without revealing or requiring the description of a component's internal operation. Both collections of sequential processes and the data objects which they share may be described. The scheme is of particular value during the early stages of software system design, when the system's modules are being delineated and their interactions designed, and when rigorous, well-defined specification of undesigned components allows formal and informal arguments concerning the design's correctness to be formulated.