University of Minnesota
Software Engineering Center

You are here

Sanjai Rayadurgam

Photo of Sanjai Rayadurgam
Staff Member
Phone Number: 
Office Location: 
6-202 Keller Hall

Sanjai Rayadurgam is a Research Project Specialist at the University of Minnesota Software Engineering Center. His research interests are in software testing, formal analysis and requirements modeling, with particular focus on safety-critical systems development, where he has significant industrial experience. He earned a B.Sc. in Mathematics from the University of Madras at Chennai, and in Computer Science & Engineering, an M.E. from the Indian Institute of Science at Bangalore and a Ph.D. from the University of Minnesota at Twin Cities. He is a member of IEEE and ACM.

Recent Publications

Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow Language

We report on our experience with using the PVS theorem prover as a verification tool for analyzing systems modelled in RSML-e - a synchronous dataflow language. RSML-e is a formal specification language particularly well-suited for specifying requirements of reactive systems. We advocate a specification-centered approach to system development, in which various development activities like prototyping, analysis, verification, testing, and code-generation are based on a formal model of the system requirements.

Auto-Generating Test Sequences using Model Checkers: A Case Study

Use of model-checking approaches for test generation from requirement models have been proposed by several researchers. These approaches leverage the witness (or counter-example) generation capability of model-checkers for constructing test cases. Test criteria are expressed as temporal properties. Witness traces generated for these properties are instantiated to create complete test sequences, satisfying the criteria. State-space explosion can, however, adversely impact model-checking and hence such test generation. Thus, there is a need to

Toward Automation for Model Checking Requirement Specifications with Numeric Constraints

Model checking techniques have not been effective in important classes of software systems---systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the system variables. Various model abstraction techniques have been proposed to address this problem, but their effectiveness in practice is limited by two factors; first, the abstraction process is manual and requires a great deal of ingenuity, and, second, the abstraction may be coarse and introduce too many spurious behaviors to provide meaningful analysis results.