กก
|
Research
Interests
- Verification of autonomous systems
- System Modeling
- Formal Methods
- Software Engineering
- Component-based Development
Tools (collaborated)
- SpecCC. A tool for consistency checking of requirements in natural language.
- DFinder. A toolset for compositional
deadlock detection and verification.
- CTAV/LTL. An
LTL model checker for real time systems modeled by closed timed automata.
- CTAV/Reach. A tool for reachability analysis of real time systems modeled
by closed timed automata.
- FPTA. A verifier for reachability analysis of real time systems modeled
by finite precision timed automata.
- XYZ/E
development environment.
Recent
Papers
Journal papers
- Saddek Bensalem, Lavindra De Silva, Felix Ingrand, and Rongjie Yan.
A Verifiable and Correct-by-Construction Controller for Robot Functional Levels. Joser, 2011, Vol 2, No 1:1-19(pdf).
- De Ma, Rongjie Yan, Kai Huang, Min Yu, Haitong Ge, Xiaolang Yan, A. Jerraya. Performance Estimation Techniques with MPSoC Transaction-Accurate Model. TCAD, 2013,32(12):1920-1933.
- Rongjie Yan, Min Yu, Kai Huang, Xiaomeng Zhang. Communication-oriented performance optimisation during code generation from Simulink models. IJES, 2014 6(2/3): 124-134.
.
- Kai Huang, Min Yu, Rongjie Yan, Xiaomeng Zhang, Xiaolang Yan, Lisane B. de Brisolara, Ahmed Amine Jerraya, Jiong Feng. Communication Optimizations for Multithreaded Code Generation from Simulink Models. TECS, 2015, 14(3): 59:1-59:26.
.
- Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan. Component-based verification using incremental design and invariants. SoSYM, 2016, 15(2): 427-451.
.
Conference
papers
- Rongjie Yan, Anyu Cai, Hongyu Gao, Feifei Ma, Jun Yan. SMT-based Multi-objective Optimization for Scheduling of MPSoC Applications. TASE 2019.
- Rongjie Yan, Junjie Yang, Di Zhu, Kai Huang: Design verification and validation for reliable safety-critical autonomous control systems. ICECCS 2018: 170-179.
- Rongjie Yan, Di Zhu, Fan Zhang, Yiqi Lv, Junjie Yang, Kai Huang: Resource-Aware Design for Reliable Autonomous Applications with Multiple Periods. FM 2018: 294-311.
- Dong Yan, Linjie Pan, Rongjie Yan, Jun Yan, Jian Zhang:
Comprehensive Static Analysis for Configurable Software via Combinatorial Instantiation. COMPSAC (1) 2017: 67-74.
- Rongjie Yan, Yupeng Zhou, Yige Yan, Minghao Yin, Min Yu, Feifei Ma, Kai Huang:
A Hybrid Multi-objective Evolutionary Algorithm for Energy-Aware Allocation and Scheduling Optimization of MPSoCs. ICTAI 2017: 701-708.
- Rongjie Yan, Chih-Hong Cheng, Yesheng Chai:
Formal consistency checking over specifications in natural languages. DATE 2015: 1677-1682.
- Xueyang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang, Wenhui Zhang, Guangquan Zhang:
Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking. FM 2015: 551-569.
- Lavindra de Silva, Rongjie Yan, Felix Ingrand, Rachid Alami, Saddek Bensalem:
A Verifiable and Correct-by-Construction Controller for Robots in Human Environments. HRI (Extended Abstracts) 2015: 281.
- Rongjie Yan, De Ma, Kai Huang, Xiaoxu Zhang, Siwen Xiu: Annotation and analysis combined cache modeling for native simulation. ASP-DAC 2014: 406-411.
- Rongjie Yan, Kai Huang, Min Yu, Xiaomeng Zhang. Communication pipelining for Code Generation from Simulink Models. TrustCom/ISPA/IUCC 2013: 1893-1900.
- Chih-Hong Cheng, Rongjie Yan, Harald Ruess, Saddek Bensalem. Distributed Priority Synthesis using Knowledge. AGERE!@SPLASH 2012.
- Chih-Hong Cheng, Rongjie Yan, Saddek Bensalem, Harald Ruess: Distributed Priority Synthesis. The 7th International Conference on Systems Software Verification. SSV 2012: 57-72.
- Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl and Alois knoll.
Algorithms for Synthesizing Priorities in Component-based Systems.
ATVA11.
- Saddek Bensalem, Lavindra De Silva, Andreas Griesmayer, Felix Ingrand, Axel Legay and Rongjie Yan.
A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems
SC11.
- Saddek Bensalem, Andreas Griesmayer, Axel Legay,
Thanh-Hung Nguyen, Joseph Sifakis and Rongjie Yan. D-Finder 2: Towards
Efficient Correctness of Incremental Design. NASA Formal Methods 2011:
453-458.
- Chih-Hong Cheng, Saddek Bensalem, Barbara Jobstmann,
Rongjie Yan, Alois Knoll and Harald Ruess. Model Construction and
Priority Synthesis for Simple Interaction Systems. NASA Formal Methods
2011: 466-471.
- Saddek Bensalem, Marius Bozga, Axel Legay, Thanh Hung
Nguyen, Joseph Sifakis and Rongjie Yan. Incremental Component-based
Construction and Verification using Invariants.
FMCAD10 .
- Saddek Bensalem, Axel Legay, Thanh Hung Nguyen, Joseph
Sifakis and Rongjie Yan. Incremental Invariant Generation for
Compositional Design.
TASE10.
- Saddek Bensalem, Lavindra de Silva, Matthieu Gallien,
Felix Ingrand, Rongjie Yan. ``Rock Solid'' Software: A Verifiable
and
Correct-by-Construction Controller for Rover and
Spacecraft Functional Levels.
ISAIRAS10.
- Saddek Bensalem, Lavindra de Silva, Matthieu Gallien,
Felix Ingrand, Rongjie Yan. A Verifiable and Correct by
Construction Controller for Robots in Human Environment.
DRHE10.
- Rongjie Yan, Guangyuan Li, Wenliang
Zhang and Yunquan Peng. Improvements
for the Symbolic Verification of Timed Automata(pdf,
slide).
FORTE07.
- Rongjie
Yan, Guangyuan Li, Zhisong
Tang. Symbolic Model Checking of Finite Precision Timed Automata(pdf,slide).
ICTAC05.
Papers in Chinese
- Rongjie
Yan, Wenliang Zhang, Zhisong
Tang.
Truly Bitstate-hashing for SCC-based Emptiness
Checking Algorithms, Chinese Journal of Computers, 2008, 6: 979-988.
- Rongjie
Yan, Guangyuan Li, Yubo
Xu, Chunming Liu, Zhisong Tang. Reachability Checking of Finite Precision
Timed Automata. Software Journal, 2006, 17(1): 1-10.
- Rongjie
Yan, Guangquan Zhang. Component-based Software
Architecture Refinement and Its Application. Journal of Chongqing Normal
University (Natural Science Edition), 2003, 20(2): 1-5.
Techniques
Reports
- Saddek Bensalem, Axel Legay, Thanh Hung Nguyen, Joseph
Sifakis and Rongjie Yan. Incremental Invariant Generation for
Compositional Design, Verimag Technical Report number TR-2010-6,
Feb, 2010.
- Saddek
Bensalem, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan: Incremental Component-based
Construction and Deadlock Checking, Verimag Technical Report number TR-2009-12,
Sep 2009.
- Rongjie
Yan, Chunming Liu, Yubo
Xu. User Manual for FPTA Verifier. Technical
Reports of State Key Laboratory of Computer Science, ISCAS-LCS-04-01 (in
Chinese).
Invited Talks
- XYZ
System and its Features, Jun. 2008, Xi'an
- Concurrent
System Modeling and Verification, May 2005, Suzhou
Some Links
CADP case studies, BEEP case studies
Spin, Uppaal, NuSMV, CUDD manual,
LTL to automata
C Minor, Coq Cooker, Coq online
Compcert C, Online document
Online dictionary
Publication resources
Software theory, Dates of conferences
Software engineering, Dates of conferences
High performance computing, Dates of conferences
|