In this paper, we review current requirements engineering (RE) research and identify future
research directions suggested by emerging software needs. First, we overview the state of …

Requirements engineering (RE) is concerned with the identification of the goals to be
achieved by the envisioned system, the operationalization of such goals into services and …

A comprehensive introduction to the foundations of model checking, a fully automated
technique for finding flaws in hardware and software; with extensive examples and both …

We show how a very modest modification to a typical modern SAT-solver enables it to solve
a series of related SAT-instances efficiently. We apply this idea to checking safety properties …

Even well administered networks are vulnerable to attacks due to the security ramifications
of offering a variety of combined services. That is, services that are secure when offered in …

We apply a model checker to the problem of test generation using a new application of
mutation analysis. We define syntactic operators, each of which produces a slight variation …

The development of complex software systems is a complex and lengthy activity that
involves the participation and collaboration of many stakeholders (eg customers, users …

This paper presents a symbolic model checking algorithm for continuous-time Markov
chains for an extension of the continuous stochastic logic CSL of Aziz et al [1]. The …

Two translations from activity diagrams to the input language of NuSMV, a symbolic model
verifier, are presented. Both translations map an activity diagram into a finite state machine …

To formally verify a large software application, the standard method is to invest a
considerable amount of time and expertise into the manual construction of an abstract …