University of Minnesota
Software Engineering Center
/

You are here

Sanjai Rayadurgam

Photo of Sanjai Rayadurgam
Director of the Software Engineering Center
Phone Number: 
612-625-0331
Office Location: 
6-202 Keller Hall
Education: 
B.Sc. in Mathematics, University of Madras, Chennai (1989)
M.E. in Computer Science and Engineering, Indian Institute of Science, Bengaluru (1993)
Ph.D. in Computer and Information Sciences, University of Minnesota, Minneapolis (2004)
Biography: 

Sanjai Rayadurgam is the director of the University of Minnesota Software Engineering Center and is a Research Project Specialist in the Department of Computer Science and Engineering. His research interests are in software testing, formal analysis and requirements modeling, with particular focus on safety-critical systems development. Prior to his work at the University of Minnesota, he worked at Boston Scientific, performing advanced tools development, systems engineering, and verification and validation of implantable cardiac device. He For his doctoral dissertation he developed techniques to automatically derive tests from behavioral models of software that could meet stringent coverage criteria. He has co-authored several research papers and articles in software engineering. He was a co-organizer of Dagstuhl seminar on Software and Systems Traceability for Safety-Critical Projects in 2015, was a program co-chair for the NASA Formal Methods Symposium in 2016 and is in the program committees of various workshops and conferences in software engineering.

Research: 
His recent research areas include contract-discovery and coverage techniques for black-box object-code components funded by a NSF grant, test generation and verification of plan executions for autonomy platforms funded by a NASA grant, testing techniques of learning enabled components for assuring autonomous systems funded under a DARPA project and model based fuzz testing funded under an ONR project.
Interests: 
Software Engineering, Formal Methods, Automated Testing, High Assurance Autonomy

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.

Pages