Software testing can only be formalized and quantified when a solid basis for test generation can be defined. Bases that are commonly used include the source code, control flow graphs, design representations, and specifications/requirements. Formal specifications represent a significant opportunity for testing because they precisely describe what functions the software is supposed to provide in a form that can be easily manipulated. In this paper, we present a new method for generating tests from formal specifications. This method is comprehensive in specification coverage, applies at several levels of abstraction, and can be highly automated. We apply our method to SOFL specifications, describe the technique, and demonstrate the application on a case study. A preliminary evaluation using a code-level coverage criterion (mutation testing), indicates that the method can result in very effective tests.

Proactive secret sharing deals with refreshing secret shares, i.e., redistributing the shares of a secret to the original access structure. In this paper we focus on the general problem of redistributing shares of a secret key. Shares of a secret have been distributed such that access sets specified in the access structure (e.g., t-out-of-l) can access (or use) the secret. The problem is how to redistribute the secret, without recovering it, in such a way that those specified in the new access structure will be able to recover the secret. We also adapt our scheme such that it can be used in the context of threshold cryptography and discuss its applications to secure databases.