Articles written in Sadhana
Volume 17 Issue 1 March 1992 pp 1-28
In this paper, we discuss the issues and challenges that lie in the specification, development, and verification of real-time systems. In our presentation, we emphasize on the issues underlying modelling of real-time distributed concurrency.
Volume 21 Issue 2 April 1996 pp 185-211 Software Specification, Verification And Validation
In this paper, we use perfectly synchronous languages such as
Volume 44 Issue 1 January 2019 Article ID 0018
This paper proposes a novel notion called variability verification applicable to Software Product Lines (SPL). Variability is central to SPL and we have observed that variability is expressed differently at different levels of abstraction in the development flow of SPL. A natural problem in this context is theconformance of variability information expressed at different levels. Design variability verification, in particular, checks whether the variability expressed at the design level conforms to that at the requirement level. Unlike many existing approaches to SPL modelling, our work does not assume a single global view of variation points, even within the same level of abstraction. In our view, an SPL is a concurrent composition of features, where each feature exhibits independent variability. This enables incremental addition of variability. The procedure iscompositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. Feature level verification essentially involves standard model checking while, in the second step, a Quantified Boolean Formula (QBF) is synthesized and solved. The method has been implemented and demonstrated in a tool SPL Engine for Design Verification (SPLEnD) on a couple of fairly large case studies. SPLEnD uses SPIN tool for the feature level conformance, while the state-of-the-art QBFsolver CirQit is used for the SPL level conformance. SPLEnD easily handles the evolution of SPL by addition of new features and modification of existing features. Experimental results with SPLEnD look very promising.