Travelled to:
1 × Australia
1 × Belgium
1 × Denmark
1 × Finland
1 × Germany
1 × Ireland
1 × Japan
1 × Norway
1 × Republic of China
1 × Sweden
1 × The Netherlands
2 × Canada
2 × China
2 × Italy
2 × Russia
2 × Switzerland
3 × France
4 × United Kingdom
9 × USA
Collaborated with:
J.Sun Y.Liu B.P.Mahony H.H.Wang J.Sun ∅ S.Qin T.K.Nguyen Y.Li L.Gui É.André S.Song S.Lin S.J.Zhang Z.Xing N.N.Tun S.Liu R.Duke S.Liu B.Wadhwa J.Pang C.H.Lee T.H.Tan M.Chen M.Zheng C.Chen H.Liang D.Lucanu W.Chin N.Fulton X.Wang Y.Xue Y.L.0001 J.S.0001 W.Zhao L.Li Y.Wu P.Hao X.Zhang Y.Liu A.Roychoudhury S.Liu H.B.Lee C.Sun J.Ma Y.J.Si D.Sanán Y.Gu J.Hao H.Leung W.Chen Y.A.Liu L.Tran G.Bai H.Wang Y.Zhang Y.Lin X.Peng C.Choppy G.Meng X.P.0001 Y.L.0003
Talks about:
model (14) system (12) time (10) semant (8) check (6) softwar (5) formal (5) verif (5) state (5) tcoz (5)
Person: Jin Song Dong
DBLP: Dong:Jin_Song
Contributed to:
Wrote 54 papers:
- FM-2015-LiSLD #protocol #security #verification
- Verifying Parameterized Timed Security Protocols (LL, JS, YL, JSD), pp. 342–359.
- ISSTA-2015-GuiSLD #abstraction #assessment #communication #distributed #refinement #reliability
- Reliability assessment for distributed systems via communication abstraction and refinement (LG, JS, YL, JSD), pp. 293–304.
- ISSTA-2015-TanXCSLD #algorithm #optimisation
- Optimizing selection of competing features via feedback-directed evolutionary algorithms (THT, YX, MC, JS, YL, JSD), pp. 246–256.
- ASE-2014-LiuSLZWDW #automation #case study #detection #documentation #fault
- Automatic early defects detection in use case documents (SL, JS, YL, YZ, BW, JSD, XW), pp. 785–790.
- FSE-2014-Gui00ND #agile #analysis #named #nondeterminism #reliability #tool support
- RaPiD: a toolkit for reliability analysis of non-deterministic systems (LG, JS, YL, TKN, JSD), pp. 727–730.
- ICSME-2014-LinXPL0ZD #maintenance #named
- Clonepedia: Summarizing Code Clones by Common Syntactic Context for Software Maintenance (YL, ZX, XP, YL, JS, WZ, JSD), pp. 341–350.
- ASE-2013-Wu0LD #analysis #automation #component #dependence #using
- Automatically partition software into least privilege components using dynamic data dependency analysis (YW, JS, YL, JSD), pp. 323–333.
- ASE-2013-Zhang0SLMD #automation #constraints #detection #symmetry
- Constraint-based automatic symmetry detection (SJZ, JS, CS, YL, JM, JSD), pp. 15–25.
- CAV-2013-AndreLSDL #concurrent #named #parametricity #realtime #synthesis
- PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems (ÉA, YL, JS, JSD, SWL), pp. 984–989.
- ESEC-FSE-2013-LiuL0ZWD #model checking #named #self #state machine #uml
- USMMC: a self-contained model checker for UML state machines (SL, YL, JS, MZ, BW, JSD), pp. 623–626.
- ICSE-2013-DongSL #model checking
- Build your own model checker in one month (JSD, JS, YL), pp. 1481–1483.
- ICSE-2013-TanA00DC #composition #synthesis
- Dynamic synthesis of local time requirement for service composition (THT, ÉA, JS, YL, JSD, MC), pp. 542–551.
- IFM-2013-LiuLACSWD #semantics #state machine #uml
- A Formal Semantics for Complete UML State Machines with Communications (SL, YL, ÉA, CC, JS, BW, JSD), pp. 331–346.
- IFM-2013-Song00LD #analysis #divide and conquer #reachability
- Improved Reachability Analysis in DTMC via Divide and Conquer (SS, LG, JS, YL, JSD), pp. 162–176.
- ISSTA-2013-GuiSLSDW #model checking #predict #reliability #testing
- Combining model checking and testing with an application to reliability prediction and distribution (LG, JS, YL, YJS, JSD, XW), pp. 101–111.
- VMCAI-2013-ZhengS0LD0 #network #partial order #reduction #using
- State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction (MZ, DS, JS, YL, JSD, YG), pp. 515–535.
- CAV-2012-SongSLD #model checking #probability #realtime
- A Model Checker for Hierarchical Probabilistic Real-Time Systems (SS, JS, YL, JSD), pp. 705–711.
- FM-2012-LinLSDA #automation #composition #verification
- Automatic Compositional Verification of Timed Systems (SWL, YL, JS, JSD, ÉA), pp. 272–276.
- FM-2012-NguyenSLDL #analysis
- Improved BDD-Based Discrete Analysis of Timed Systems (TKN, JS, YL, JSD, YL), pp. 326–340.
- ICSE-2012-SongHLSLD #approach #model checking #multi #probability
- Analyzing multi-agent systems with probabilistic model checking approach (SS, JH, YL, JS, HfL, JSD), pp. 1337–1340.
- ASE-2011-NguyenSLD #framework #model checking
- A model checking framework for hierarchical systems (TKN, JS, YL, JSD), pp. 633–636.
- FM-2011-ZhangSPLD #on the #reduction
- On Combining State Space Reductions with Global Fairness Assumptions (SJZ, JS, JP, YL, JSD), pp. 432–447.
- ASE-2010-XingSLD #debugging #named #specification
- SpecDiff: debugging formal specifications (ZX, JS, YL, JSD), pp. 353–354.
- FSE-2010-LiuSD #realtime
- Analyzing hierarchical complex real-time systems (YL, JS, JSD), pp. 365–366.
- CAV-2009-SunLDP #flexibility #named #towards #verification
- PAT: Towards Flexible Verification under Fairness (JS, YL, JSD, JP), pp. 709–714.
- FM-2009-SunLRLD #abstraction #model checking #process
- Fair Model Checking with Process Counter Abstraction (JS, YL, AR, SL, JSD), pp. 123–139.
- SEKE-2009-ZhangLSDCL #scalability #verification
- Formal Verification of Scalable NonZero Indicators (SJZ, YL, JS, JSD, WC, YAL), pp. 406–411.
- ICSE-2008-ChenDS #calculus #verification
- A verification system for timed interval calculus (CC, JSD, JS), pp. 271–280.
- KR-2008-TunD #generative #ontology #reuse
- Ontology Generation through the Fusion of Partial Reuse and Relation Extraction (NNT, JSD), pp. 318–328.
- SEKE-2007-LiangDS #evolution #monitoring #runtime
- Evolution and Runtime Monitoring of Software Systems (HL, JSD, JS), pp. 343–348.
- ICSE-2006-Dong #modelling #semantics #specification #web
- From semantic web to expressive software specifications: a modeling languages spectrum (JSD), pp. 1063–1064.
- ICSE-2006-DongHZQ #modelling #named
- HighSpec: a tool for building and checking OZTA models (JSD, PH, XZ, SQ), pp. 775–778.
- FM-2005-SunD #distributed #process #specification #synthesis
- Synthesis of Distributed Processes from Scenario-Based Specifications (JS, JSD), pp. 415–431.
- SEKE-2005-LucanuLD #morphism #owl
- Institution Morphisms for Relating OWL and Z (DL, YFL, JSD), pp. 286–291.
- SEKE-2005-WangDS #alloy #reasoning #using
- Reasoning Support for SWRL-FOL Using Alloy (HHW, JSD, JS), pp. 626–631.
- SEKE-2005-WangDSL #approach #design #process
- TCOZ Approach to OWL-S Process Model Design (HHW, JSD, JS, YFL), pp. 354–359.
- ICSE-2004-Dong #modelling #semantics #web
- Software Modeling Techniques and the Semantic Web (JSD), pp. 724–725.
- ICSE-2004-DongLLW #verification
- Verifying DAML+OIL and Beyond in Z/EVES (JSD, CHL, YFL, HHW), pp. 201–210.
- IFM-2004-DongQS #generative #specification
- Generating MSCs from an Integrated Formal Specification Language (JSD, SQ, JS), pp. 168–186.
- FME-2003-DongSW #alloy #reasoning #semantics #web
- Checking and Reasoning about Semantic Web through Alloy (JSD, JS, HHW), pp. 796–813.
- FME-2003-QinDC #programming #semantics
- A Semantic Foundation for TCOZ in Unifying Theories of Programming (SQ, JSD, WNC), pp. 321–340.
- SEKE-2003-DongSWLL #alloy #case study #ontology #web
- Analysing Web Ontology in Alloy: A Military Case Study (JSD, JS, HHW, CHL, HBL), pp. 542–546.
- FME-2002-DongSW #semantics #web
- Semantic Web for Extending and Linking Formalisms (JSD, JS, HHW), pp. 587–606.
- ICSE-2001-Dong #diagrams #modelling
- State, Event, Time and Diagram in System Modeling (JSD), pp. 733–734.
- FM-v2-1999-DongMF #modelling
- Modeling Aircraft Mission Computer Task Rates (JSD, BPM, NF), p. 1855.
- FM-v2-1999-MahonyD
- Sensors and Actuators in TCOZ (BPM, JSD), pp. 1166–1185.
- IFM-1999-DongL #semantics
- An Object Semantic Model of SOFL (JSD, SL), pp. 189–208.
- IFM-1999-MahonyD #overview #semantics
- Overview of the Semantics of TCOZ (BPM, JSD), pp. 66–85.
- ICSE-1998-MahonyD #csp
- Blending Object-Z and Timed CSP: An Introduction to TCOZ (BPM, JSD), pp. 95–104.
- TOOLS-PACIFIC-1993-DongD #morphism #polymorphism
- Class Union and Polymorphism (JSD, RD), pp. 181–190.
- ASE-2015-LinSNLD #composition #verification
- Interpolation Guided Compositional Verification (T) (SWL, JS, TKN, YL, JSD), pp. 65–74.
- ASE-2017-LinMXXSPLZD #design #mining #reuse
- Mining implicit design templates for actionable code reuse (YL0, GM, YX, ZX, JS0, XP0, YL0, WZ, JSD), pp. 394–404.
- ASE-2018-Lin0TBWD #debugging #slicing
- Break the dead end of dynamic slicing: localizing data and control omission bug (YL0, JS0, LT, GB, HW, JSD), pp. 509–519.