Area of Interest

My research is in the broad area of system verification with a focus on model checking and runtime verification. Model checking refers to the following problem: given a model of a system, exhaustively and automatically check whether this model meets a given specification. Runtime verification is a system analysis approach based on extracting information from a running system and using it to detect observed behaviors satisfying or violating certain properties. Here is my CV.

Projects

  • Parameter Synthesis for Flocking Model using Genetic Algorithm
  • AADL to UPPAAL Translator
  • Publications

  • Radu Grosu, Doron Peled, C.R. Ramakrishnan, Scott A. Smolka, Scott D. Stoller, and Junxing Yang, “Using Statistical Model Checking for Measuring Systems”, ISoLA 2014, LNCS 8803, pp. 223-238, 2014.
  • Siddhartha Bhattacharyya,Steven Miller,Junxing Yang,Scott Smolka,Baoluo Meng, Christoph Sticksel, Cesare Tinelli, “Verification of quasi-synchronous systems with Uppaal”, Digital Avionics Systems Conference (DASC), 2014 IEEE/AIAA 33rd. IEEE, 2014.
  • Radu Grosu, Doron Peled, C.R. Ramakrishnan, Scott A. Smolka, Scott D. Stoller, and Junxing Yang, “Compositional Branching-Time Measurements”, FPS 2014 (Sifakis Festschrift), LNCS 8415, pp. 118-128, 2014.
  • Patent

    Jinshuo Liu, Juan Deng, Li Yan, Junxing Yang, Yangyang Lu and Yulong Zhang, “Model and Algorithm for Automated Item Generator of the Graphic Intelligence Test”, United States Patent Application, US-2012-0005143-A1