3,458 papers · page 156 of 173
Nowadays component-based technologies offer straightforward ways of building applications from existing components. Although these technologies might differ in terms of the level of heterogeneity among components they support, e.g. CORBA or COM versus J2EE, they all suffer the pr…
Detecting symmetries in the structure of systems is a well known technique falling in the class of bisimulation (strongly) preserving state space reductions. Previous work in applying symmetries to aid model checking focuses mainly on process topologies and user specified data ty…
Designing and implementing security-critical systems correctly is difficult. In practice, most vulnerabilities arise from bugs in implementations. We present work towards systematic specification-based testing of security-critical systems using the CASE tool AutoFocus. Cryptograp…
Summary form only given. System level design is nowadays a complex process due to heterogeneity of domains of components in a single system. The language standard, Rosetta, was proposed as a means to help in such designs. An important feature in Rosetta is known as domain interac…
Summary form only given. The research to merge the relatively simple and graphical nature of UML with the firm semantics bases of B has been mentioned several time in the literature. The goal is to propose automatic derivation schemes from UML to B specifications. Then, the const…
An appropriate approach for translating UML to B formal specifications allows one to use UML and B jointly in a unified, practical and rigorous software development. We formally analyze UML specifications via their corresponding B formal specifications. This point is significant …
Nowadays, test cases may correspond to elaborate programs. It is therefore sensible to try to specify test cases in order to get a more abstract view of these. This paper explores the notion of test purpose as a way to specify a set of test cases. It shows how test purposes are e…
Many formal specification languages have been developed to engineer complex systems. However natural language (NL) has remained the choice of domain experts to specify the system because formal specification languages are not easy to master. Therefore NL requirements documentatio…
The paper presents an original method to generate test sequences. From formal specifications of the system to be tested, an equivalent system of constraints is derived, and then the domain of each state variable of this system is partitioned into subdomains. Using this partition,…
Test suites are designed to validate the operation of a system against requirements. One important aspect of a test suite design is to ensure that system operation logic is tested completely. This is a difficult task. Code coverage tools support test suite designers by providing …
The Java programming language supports monitors. Monitor implementations, like other concurrent programs, are hard to test due to the inherent non-determinism. This paper presents the ConAn (Concurrency Analyser) tool for generating drivers for the testing of Java monitors. To ob…
Proof-checking code for compliance to safety policies potentially enables a product-oriented approach to certain aspects of software certification. To date, previous research has focused on generic, low-level programming-language properties such as memory type safety. In this pap…
Source code duplication occurs frequently within large software systems. Pieces of source code, functions, and data types are often duplicated in part or in whole, for a variety of reasons. Programmers may simply be reusing a piece of code via copy and paste or they may be "re-in…
We present TestEra, a novel framework for automated testing of Java programs. TestEra automatically generates all non-isomorphic test cases within a given input size and evaluates correctness criteria. As an enabling technology, TestEra uses Alloy, a first-order relational langua…
Generative programming methods provide some significant advantages for the repeated deployment of product line architectures. The paper considers XML as a tool for building and describing applications that use generative programming methods. It describes techniques for the creati…
Software management oracles often contain numerous subjective features. At each subjective point, a range of behaviors is possible. Stochastic simulation samples a subset of the possible behaviors. After many such stochastic simulations, the TAR2 treatment learner can find contro…
Software engineers building a complex system make use of a number of informal and semi-formal notations. We describe a framework, xlinkit, for managing the consistency of development artifacts expressed in such notations. xlinkit supports distributed software engineering by provi…
Assurance of software systems has traditionally been sought through the rigour of the development process. The higher the assurance, the more demanding the development process; the highest assurance requiring the use of formal methods during development. This approach has been fo…
CafeOBJ is a wide spectrum formal specification language based on multiple logical foundations: mainly initial and hidden algebra. A wide range of systems can be specified in CafeOBJ thanks to its multiple logical foundations. However, distributed real-time systems happen to be e…
The paper presents new techniques for specification based-testing of synchronous software with the Lutess tool. Lutess provides a framework consisting of automatically building generators which interact with the software under test and feed it with test input sequences. In the pa…