
Overview
overview
- Dr. He received his BS and MS degrees in computer science from Nanjing University, China in 1982 and 1984 respectively; and his Ph.D. degree in computer science from Virginia Tech in 1989. He has joined FIU in 2000 after spending 10 years on the faculty at North Dakota State University. Dr. He’s research interests are in software engineering, especially formal methods. He is an internationally known expert on Petri nets. He has published 150 papers in international journals and conferences and served on more than 80 international conference program committees. He serves on the editorial board of the Transactions on Petri Nets and Other Concurrency Models and several other journals. His research has been funded by several major federal agencies including NSF, NASA, ONR, AFRL, and DOE. Dr. He has been a major adviser of 14 Ph.D. and 36 MS graduates.
research interests
- Software Engineering, Formal Methods, Software Testing, Petri Nets, Cybersecurity
Scholarly & Creative Works
selected publications
-
Article
-
2018Formal Modeling and Analysis of Collaborative Humanoid RoboticsFull Text via DOI: 10.4018/ijrat.2018010103
-
2015A Methodology to Analyze Multi-Agent Systems Modeled in High Level Petri NetsFull Text via DOI: 10.1142/S0218194015500230 Web of Science: 000368434300005
-
2013A COMPREHENSIVE SURVEY OF PETRI NET MODELING IN SOFTWARE ENGINEERINGFull Text via DOI: 10.1142/S021819401340010X Web of Science: 000324389000002
-
2012A METHODOLOGY FOR MODELING MULTI-AGENT SYSTEMS USING NESTED PETRI NETSFull Text via DOI: 10.1142/S0218194012500246 Web of Science: 000315689400002
-
2010FORMAL SPECIFICATION AND ANALYSIS OF AN AGENT-BASED MEDICAL IMAGE PROCESSING SYSTEMFull Text via DOI: 10.1142/S021819401000475X Web of Science: 000281358300002
-
2009A methodology for evaluating test coverage criteria of high level Petri netsFull Text via DOI: 10.1016/j.infsof.2009.06.014 Web of Science: 000270619300004
-
2009Flexible coordinator design for modeling resource sharing in multi-agent systemsFull Text via DOI: 10.1016/j.jss.2009.04.054 Web of Science: 000270628100012
-
2006A formal model-based approach for developing an interoperable mobile agent systemFull Text via DOI: 10.3233/MGS-2006-2407 Web of Science: 000212571500007
-
2004Formally analyzing software architectural specifications using SAMFull Text via DOI: 10.1016/S0164-1212(02)00087-0
-
2003A new approach to verify rule-based systems using petri netsFull Text via DOI: 10.1016/S0950-5849(03)00058-2
-
2002A methodology of testing high-level Petri netsFull Text via DOI: 10.1016/S0950-5849(02)00048-4
-
2001PZ nets - a formal method integrating Petri nets with ZFull Text via DOI: 10.1016/S0950-5849(00)00134-8
-
2000SPECIFYING SOFTWARE ARCHITECTURAL CONNECTORS IN SAMFull Text via DOI: 10.1142/s0218194000000201
-
2000Specifying software architectural connectors in SAMFull Text via DOI: 10.1016/S0218-1940(00)00020-1
-
2000Translating hierarchical predicate transition nets to CC++ programsFull Text via DOI: 10.1016/S0950-5849(99)00103-2 Web of Science: 000086895100003
-
1999Introducing software architecture specification and analysis in SAM through an exampleFull Text via DOI: 10.1016/S0950-5849(99)00009-9 Web of Science: 000080581300005
-
1997Mapping Petri nets to concurrent programs in CC++Full Text via DOI: 10.1016/S0950-5849(97)00006-2
-
1991A methodology for constructing predicate transition net specificationsFull Text via DOI: 10.1002/spe.4380210806
-
-
Book
-
Book Chapter
-
2019A Personal Journey in Petri Net Research. 111-115.Full Text via DOI: 10.1007/978-3-319-96154-5_15
-
2019Formal Modeling and Analysis of Collaborative Humanoid Robotics. 1086-1108.Full Text via DOI: 10.4018/978-1-5225-8060-7.ch051
-
2010Architecture-centered integrated verification. 104-124.Full Text via DOI: 10.4018/978-1-60960-215-4.ch005
-
2010Towards Rewriting Semantics of Software Architecture SpecificationFull Text via DOI: 10.5772/7520
-
2009Formal methods for specifying and analyzing complex software systems. 243-264.Full Text via DOI: 10.4018/978-1-59904-630-3.Ch017
-
2006Formal methods for specifying and analyzing complex software systems. 319-345.Full Text via DOI: 10.4018/978-1-59140-941-1.ch013
-
2006Formal methods for specifying and analyzing complex software systems. 123-150.Full Text via DOI: 10.1007/1-4020-4223-X_6
-
2005A methodology of component integration testing. 239-269.Full Text via DOI: 10.1007/3-540-27071-X_12
-
20059 High-Level Petri Nets-Extensions, Analysis, and Applications. 459-475.Full Text via DOI: 10.1016/b978-012170960-0/50035-9
-
2005High-Level Petri Nets-Extensions, Analysis, and Applications. 459-475.Full Text via DOI: 10.1016/B978-012170960-0/50035-9 Web of Science: 000311291700034
-
2002Modeling and Analyzing the Software Architecture of a Communication Protocol Using SAM. 63-77.Full Text via DOI: 10.1007/978-0-387-35607-5_4
-
2001Object Orientation in Hierarchical Predicate Transition Nets. 196-215.Full Text via DOI: 10.1007/3-540-45397-0_6
-
-
Conference
-
2021Modeling Cyber Physical Systems with Learning Enabled Components using Hybrid Predicate Transition Nets. 1099-1108.Full Text via DOI: 10.1109/QRS-C55045.2021.00164 Web of Science: 000808814500152
-
2020Modeling and Analyzing Smart Contracts using Predicate Transition Nets. 108-115.Full Text via DOI: 10.1109/QRS-C51114.2020.00029 Web of Science: 000682774300017
-
2019Hybrid Predicate Transition Nets - A Formal Method for Modeling and Analyzing Cyber-Physical Systems. 216-227.Full Text via DOI: 10.1109/QRS.2019.00038 Web of Science: 000587580300024
-
2018A Method for Predicting Two-variable Atomicity Violations. 103-110.Full Text via DOI: 10.1109/QRS.2018.00024 Web of Science: 000587579900011
-
2018Modeling and Analyzing Cyber Physical Systems Using High Level Petri Nets. 469-476.Full Text via DOI: 10.1109/QRS-C.2018.00086 Web of Science: 000449555600073
-
2018A systematic approach for developing cyber physical systems. 456-461.Full Text via DOI: 10.18293/SEKE2018-004
-
2018Modeling and analyzing hybrid systems using hybrid predicate transition nets. 397-402.Full Text via DOI: 10.18293/SEKE2018-158
-
2017A Framework for Developing Cyber-Physical Systems. 1361-1386.Full Text via DOI: 10.1142/S0218194017400010 Web of Science: 000423457100002
-
2017A Method to Analyze Predicate Transition Nets Using SPIN Model Checker. 1455-1481.Full Text via DOI: 10.1142/S021819401740006X Web of Science: 000423457100007
-
2017Modeling and Analyzing the Android Permission Framework using High Level Petri Nets. 232-239.Full Text via DOI: 10.1109/QRS.2017.34 Web of Science: 000426842400026
-
2017A framework for developing cyber physical systems. 236-241.Full Text via DOI: 10.18293/SEKE2017-095
-
2017A method to analyze high level petri nets using SPIN model checker. 161-166.Full Text via DOI: 10.18293/SEKE2017-162
-
2016A Term Rewriting Approach to Analyze High Level Petri Nets. 109-112.Full Text via DOI: 10.1109/TASE.2016.11 Web of Science: 000389772000017
-
2016
-
2016Modeling and analyzing security patterns using high level petri nets. 623-627.Full Text via DOI: 10.18293/seke2016-010
-
2015A Generic Model of Execution for Synthesizing Interpreted Domain-Specific Models. 495-504.Full Text via DOI: 10.1016/j.procs.2015.08.521 Web of Science: 000364544900070
-
2015A Method for Validating Intent Model Behavior in DSVMs. 247-254.Full Text via DOI: 10.1109/HASE.2015.43 Web of Science: 000380911000031
-
2015A method for improving the precision and coverage of atomicity violation predictions. 116-130.Full Text via DOI: 10.1007/978-3-662-46681-0_8
-
2015PIPE+Verifier - A tool for analyzing high level Petri nets. 575-580.Full Text via DOI: 10.18293/SEKE2015-060
-
2014Bounded Model Checking High Level Petri Nets in PIPE plus Verifier. 348-363.Web of Science: 000347029300023
-
2012McPatom: A predictive analysis tool for atomicity violation using model checking. 191-207.Full Text via DOI: 10.1007/978-3-642-31759-0_14
-
2011
-
2011A method to mine workflows from provenance for assisting scientific workflow composition. 169-175.Full Text via DOI: 10.1109/SERVICES.2011.55
-
2011A model transformation approach for verifying multi-agent systems using SPIN. 37-42.Full Text via DOI: 10.1145/1982185.1982196
-
2010Analyzing a Formal Specification of Mondex Using Model Checking. 214-229.Web of Science: 000284034600015
-
2010A Multi-Agent Model for a Business Continuity Information Network. 657-663.Web of Science: 000391891600122
-
2008Evaluating test adequacy coverage of high level petri nets using spin. 71-78.Full Text via DOI: 10.1145/1370042.1370059
-
2008Mapping Software Architecture Specification to Rewriting Logic. 376-+.Full Text via DOI: 10.1109/QSIC.2008.16 Web of Science: 000259566300046
-
2008
-
2007A translator of software architecture design from sam to Java. 709-755.Full Text via DOI: 10.1142/S0218194007003483 Web of Science: 000253298400003
-
2007Generation of test requirements from aspectual use cases. 17-22.Full Text via DOI: 10.1145/1229384.1229388
-
2006
-
2006
-
2006Formalizing and validating UML architecture description of web systemsFull Text via DOI: 10.1145/1149993.1150002
-
2006Modeling, validating and automating composition of web services. 217-224.Full Text via DOI: 10.1145/1145581.1145626
-
2006A method for realizing software architecture design. 57-+.Web of Science: 000242539000010
-
2006An approach to web services oriented modeling and validation. 81-87.Full Text via DOI: 10.1145/1138486.1138504
-
2005Automated runtime validation of software architecture design. 446-457.Web of Science: 000235804200052
-
2005An approach to validation of software architecture model. 375-382.Web of Science: 000235436400044
-
2005An approach to validation of software architecture model. 375-382.Full Text via DOI: 10.1109/APSEC.2005.33
-
2005
-
2005Formally Modeling and analyzing a secure mobile agent finder. 47-52.Web of Science: 000235210800008
-
2004A formal approach to designing secure software architectures. 289-290.Web of Science: 000189505900039
-
2003A methodology for dependability and performability analysis in SAM. 679-688.Web of Science: 000184415300073
-
2003Pattern-based software architecture: A case study. 592-597.Full Text via DOI: 10.1109/ITCC.2003.1197596
-
2002Modeling and analyzing SMIL documents in SAM. 132-139.Web of Science: 000180301700017
-
2002Model checking software architecture specifications in SAM. 271-274.Full Text via DOI: 10.1145/568760.568808
-
2002Formal analysis of real-time systems with SAM. 275-286.Web of Science: 000181471000030
-
2002Compositional schedulability analysis of real-time systems using time Petri nets. 984-996.Full Text via DOI: 10.1109/TSE.2002.1041054
-
2001Formalizing UML semantics - Panel chair's position paper. 277-277.Web of Science: 000172264100038
-
2001An Observational Theory of Integration Testing for Component-Based Software Development. 363-368.Full Text via DOI: 10.1109/cmpsac.2001.960640
-
2000Formalizing UML class diagrams - A hierarchical predicate transition net approach. 217-222.Full Text via DOI: 10.1109/CMPSAC.2000.884721 Web of Science: 000165736000037
-
2000Constructions of behaviour observation schemes in software testing. 7-16.Full Text via DOI: 10.1109/HASE.2000.895434
-
1999
-
1999
-
1999
-
1999Pattern based software re-engineering: A case study. 300-308.Full Text via DOI: 10.1109/APSEC.1999.809616
-
1998Transformations on hierarchical predicate transition nets: Refinements and abstractions. 164-169.Full Text via DOI: 10.1109/CMPSAC.1998.716652
-
1996A formal definition of hierarchical predicate transition nets. 212-229.Full Text via DOI: 10.1007/3-540-61363-3_12
-
1996
-
1994
-
1992Structured analysis using hierarchical predicate transition nets. 212-217.Full Text via DOI: 10.1109/CMPSAC.1992.217566
-
1990
-
-
Review
-
2012Destruction of microcystins by conventional and advanced oxidation processes: A review. 3-17.Full Text via DOI: 10.1016/j.seppur.2012.02.018 Web of Science: 000303958100002
-
Works By Students
chaired theses and dissertations
- Liu, Su, Formal Modeling and Analysis Techniques for High Level Petri Nets 2014
- Zeng, Reng, Methods for Modeling and Analyzing Concurrent Software 2013
- Chang, Lily, A Nested Petri Net Framework for Modeling and Analyzing Multi-Agent Systems 2011
- Garcia, Gonzalo Argote, Formal verification and testing of software architectural models 2009
- Fu, Yujian, An integrated framework for ensuring the quality of software design 2007
- Dong, Zhijiang, A framework for transforming, analyzing, and realizing software designs in unified modeling language 2006
- Ding, Junhua, A methodology for formally modeling and analyzing software architecture of mobile agent systems 2004
- Awadallah, Amany Z., A software tool that generates symbolic model verifier (SMV) input language from a predicate transition net 2004
- Fernandez, Rigoberto, Software tool that generates hierarchical predicate transition nets (HPRTNETS) notation from a unified modeling language (UML) class diagram notation 2001
- Caldwell, William S., A formal architectural specification of the automatic validation of the Everglades National Park hydrology system 2001
- Ding, Junhua, An approach for model checking petri nets based software architecture 2000
Research
principal investigator on
- An Adaptive Evolutionary Computing Based Runtime Checker awarded by U.S. Air Force Research Laboratory 2015 - 2018
- Petri Nets Controller for Robotic Grasping awarded by National Science Foundation 2011 - 2012
- GAANN Fellowships in Computer Science at Florida International University. awarded by U.S. Department of Education 2007 - 2011
- An Integrated Software Tool for Modeling and Model-Based Control Semiconductor Manufacturing Equipment. awarded by National Science Foundation 2008 - 2009
- Distributed Flexible Resource Scheduling in Production Systems. awarded by National Science Foundation 2006 - 2008
co-principal investigator on
- Graduate Assistance in Cybersecurity and Artificial Intelligence at Florida International University awarded by U.S. Department of Education 2021 - 2024
- CREST: Center for Innovative Information Systems Engineering awarded by National Science Foundation 2008 - 2016
- GAANN Fellowship awarded by U.S. Department of Education 2009 - 2014
subproject principal investigator on
Contact
full name
- Xudong He
Identifiers
ORCID iD
- https://orcid.org/0000-0002-6676-309X (confirmed)
visualizations
publication subject areas
Citation index-derived subject areas the researcher has published in