• S Ramesh

      Articles written in Sadhana

    • Modelling real-time systems: Issues and challenges

      R K Shyamasundar S Ramesh

      More Details Abstract Fulltext PDF

      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.

    • Validation and analysis of the futurebus arbitration protocol: A case study

      F Boussinot S Ramesh RK Shyamasundar R De Simone

      More Details Abstract Fulltext PDF

      In this paper, we use perfectly synchronous languages such asEsterel, for modelling Futurebus arbitration protocol. We show that the perfect synchrony aids in the formalization, testing, validating and verifying the protocol. We discuss solutions to the above protocol and show that properties such as mutual exclusion and deadlock-freedom can be established formally. Further, we show how the simulators can be used for testing and validation and can verify an instantiation of the protocol through algebraic tools such as auto/autograph.

    • Design variability verification in Software Product Lines


      More Details Abstract Fulltext PDF

      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.

  • Sadhana | News

    • Editorial Note on Continuous Article Publication

      Posted on July 25, 2019

      Click here for Editorial Note on CAP Mode

© 2021-2022 Indian Academy of Sciences, Bengaluru.