工兵团装备保障工作流模型建立与验证
|
摘要
“管装就是管胜利,爱装就是爱生命”。随着我军现代化发展,装备管理工作日益突显出其重要的地位。近年来,我国研制和交付了一大批新型武器装备;这些新装备科技含量有很大提高,技术成分复杂,造价昂贵,对管理和使用提出了很高的要求。尤其是对于我军应对信息化条件下多种安全威胁,完成多样化任务的装备保障能力提出了新的更高的要求。在这样的背景下,我们迫切需要适应信息化发展,建立装备保障的新模式。在这个过程中装备保障工作流研究是非常关键的环节。而装备保障工作流建模更是其中具有决定意义的活动之一,可以用来优化装备保障过程、创新保障模式;也是装备保障信息化建设的顶层研究,事关装备保障的效益和信息化水平。抽象装备保障工作流模型,是实现工作流管理的前提,是完善保障机制的重要举措,符合军队发展的需要。
本文在对工兵团装备保障业务过程所包括的实力管理、勤务管理、维修管理、维修器材管理、设施设备管理、人员管理、军械管理、数据库管理、消息管理、标准管理和系统维护、辅助决策、效能评估、革新管理、知识管理等方面的分析和研究基础之上,综合运用了系统工程理论、项目管理思想和工作流建模技术,针对工兵团装备保障工作流管理的特点,考虑工兵团装备保障对团队组织的高度依赖性,建立了基于UML的工兵团装备保障工作流模型。主要通过UML的动态图来建模,用用例图描述装备保障过程需求分析;用行为图描述了装备保障业务过程间的状态转换;用交互图描述模型之间的消息传递机制。以装备维修保障为具体实例,在前面建模的基础上,采用SPIN对模型进行验证;分析UML的工作流模型的XML文件,按照规则转化(映射)成Promela的代码;再把Promela的代码输入SPIN,设置参数进行模型验证。最后总结了全文,展望了工作流的分布式建模以及模型细化和精化、工作流建模中的意外处理、一个新的工作流模型验证思路以及模型验证的自动化问题。
本文首次把UML模型和装备保障业务流程紧密结合,建立了工兵团装备保障工作流模型,并验证了所建模型。为适应任务使命牵引,创立装备保障新模式,做了非常必要的工作,促进了装备保障的信息化、高效化和决策的科学化。
"Management of equipment is management of victory, love equipment is love life." With the modernization development of our military, the management is facing higher requirements. In recent years, a large number of new weapons and equipment have been developed and delivered. Scientific and technological content of new equipment has greatly improved. At the same time the technical component is complex and costly. There are high demands to manage and use. Especially for our military to provide equipment support capability to deal with a variety of security threats, to complete the diversified tasks with the information-based conditions. It has set new and higher requirements.
Against such a background, we urgently need to adapt to information technology development, building the new model of equipment support. The equipment support workflow research is one of the key aspects of the process. Building equipment support workflow model is one of the decisive of the activities, can be used to optimize the equipment support process, innovate support model. Also is the top-level research of equipment support informationization. Bearing on the effectiveness of equipment support and the level of information.
Abstracting research equipment support workflow, is the premise of workflow management. It is an important measure to improve the support mechanism, in line with the military development. And equipment support workflow modeling is one of the decisive bearing on the effectiveness and information level of the equipment support. It is the topics that we should first study.
Based on analysis and research to the business processes of equipment support of Engineers Corps, included in the strength of management, service management, maintenance management, maintenance equipment management, facilities and equipment management, personnel management, ordnance management, database management, information management, standards of management and system maintenance, equipment support decision-making, performance assessment, innovation management, knowledge management, and so on; we established the equipment support workflow model of Engineers Corps with UML. Comprehensive used the theory of systems engineering, project management ideas and workflow modeling technology; contraposed the management features of equipment support workflow of the Engineers Corps; considered the high degree of dependence to the team organization. The UML model has been built mainly through the dynamic map. It described the needs analysis of equipment support process through the use case diagram. With the behavior diagram, it described the equipment support business processes for state transition. And with the interaction diagram, it described the model used between the message transfer. After the model had been established, used appropriate methods and tools for model validation, juat as SPIN.
Made the UML model to repair equipment as specific examples of the modeling process that had been discussed for the model validation. First of all, analyzed XML documents of the UML model. With the rules of transformation (mapping), transformed UML model into Promela code. Input Promela code into SPIN and set the parameters of model verification. Then we can give a model verification. At last, summed up the full text and looked forward to the workflow modeling and refinement of detail. And next we should study how to deal with accidents in workflow modeling; how to build the distributed model; how to get a new means of workflow model validation and how to achieve model verification automation.
In this paper, put the UML model and equipment support business processes in close connection for the first time, building the equipment support workflow model to Engineers Corps, and validated the model. It is a very necessary job that we have made to meet the mission of traction and found a new equipment support model. Promoting the informationization, efficienty and scientific decision-making on the equipment support.
本文在对工兵团装备保障业务过程所包括的实力管理、勤务管理、维修管理、维修器材管理、设施设备管理、人员管理、军械管理、数据库管理、消息管理、标准管理和系统维护、辅助决策、效能评估、革新管理、知识管理等方面的分析和研究基础之上,综合运用了系统工程理论、项目管理思想和工作流建模技术,针对工兵团装备保障工作流管理的特点,考虑工兵团装备保障对团队组织的高度依赖性,建立了基于UML的工兵团装备保障工作流模型。主要通过UML的动态图来建模,用用例图描述装备保障过程需求分析;用行为图描述了装备保障业务过程间的状态转换;用交互图描述模型之间的消息传递机制。以装备维修保障为具体实例,在前面建模的基础上,采用SPIN对模型进行验证;分析UML的工作流模型的XML文件,按照规则转化(映射)成Promela的代码;再把Promela的代码输入SPIN,设置参数进行模型验证。最后总结了全文,展望了工作流的分布式建模以及模型细化和精化、工作流建模中的意外处理、一个新的工作流模型验证思路以及模型验证的自动化问题。
本文首次把UML模型和装备保障业务流程紧密结合,建立了工兵团装备保障工作流模型,并验证了所建模型。为适应任务使命牵引,创立装备保障新模式,做了非常必要的工作,促进了装备保障的信息化、高效化和决策的科学化。
"Management of equipment is management of victory, love equipment is love life." With the modernization development of our military, the management is facing higher requirements. In recent years, a large number of new weapons and equipment have been developed and delivered. Scientific and technological content of new equipment has greatly improved. At the same time the technical component is complex and costly. There are high demands to manage and use. Especially for our military to provide equipment support capability to deal with a variety of security threats, to complete the diversified tasks with the information-based conditions. It has set new and higher requirements.
Against such a background, we urgently need to adapt to information technology development, building the new model of equipment support. The equipment support workflow research is one of the key aspects of the process. Building equipment support workflow model is one of the decisive of the activities, can be used to optimize the equipment support process, innovate support model. Also is the top-level research of equipment support informationization. Bearing on the effectiveness of equipment support and the level of information.
Abstracting research equipment support workflow, is the premise of workflow management. It is an important measure to improve the support mechanism, in line with the military development. And equipment support workflow modeling is one of the decisive bearing on the effectiveness and information level of the equipment support. It is the topics that we should first study.
Based on analysis and research to the business processes of equipment support of Engineers Corps, included in the strength of management, service management, maintenance management, maintenance equipment management, facilities and equipment management, personnel management, ordnance management, database management, information management, standards of management and system maintenance, equipment support decision-making, performance assessment, innovation management, knowledge management, and so on; we established the equipment support workflow model of Engineers Corps with UML. Comprehensive used the theory of systems engineering, project management ideas and workflow modeling technology; contraposed the management features of equipment support workflow of the Engineers Corps; considered the high degree of dependence to the team organization. The UML model has been built mainly through the dynamic map. It described the needs analysis of equipment support process through the use case diagram. With the behavior diagram, it described the equipment support business processes for state transition. And with the interaction diagram, it described the model used between the message transfer. After the model had been established, used appropriate methods and tools for model validation, juat as SPIN.
Made the UML model to repair equipment as specific examples of the modeling process that had been discussed for the model validation. First of all, analyzed XML documents of the UML model. With the rules of transformation (mapping), transformed UML model into Promela code. Input Promela code into SPIN and set the parameters of model verification. Then we can give a model verification. At last, summed up the full text and looked forward to the workflow modeling and refinement of detail. And next we should study how to deal with accidents in workflow modeling; how to build the distributed model; how to get a new means of workflow model validation and how to achieve model verification automation.
In this paper, put the UML model and equipment support business processes in close connection for the first time, building the equipment support workflow model to Engineers Corps, and validated the model. It is a very necessary job that we have made to meet the mission of traction and found a new equipment support model. Promoting the informationization, efficienty and scientific decision-making on the equipment support.
引文
[1]单志伟.装备综合保障工程[M].北京:国防工业出版社,2007,2
[2]Davenport T.H,Short J.E.The new industrial engineering:information technology and business Process redesign[J].Sloan management Review,1990,31(4):11-27
[3]张传芹.基于工作流的业务过程建模及应用研究[D].南京:东南大学,2003,4
[4]在新的起点上再创辉煌[J].通用装备保障.北京:通用装备保障编辑部,2008,6
[5]花兴来,刘庆华.装备管理工程[M].北京:国防工业出版社,2202,7
[6]李振英,卢华明,戴丽萍.管理信息系统与工作流系统的结合[J].北京:机械工业学院学报,2006,21(9)
[7]范玉顺,吴澄.工作流管理技术基础[M].北京:清华大学出版社,2001
[8]荷兰Wil Van der Aalst & Kees Van Hee著;王建民,闻立杰等译.工作流管理[M].北京:清华大学出版社,2004,1
[9]范玉顺,吴澄.工作流管理技术研究与产品现状及发展趋势[J].计算机集成制造系统-CIMS,2000,6(1):1-7
[10]蒋国银,董利红.工作流过程建模理论综述[J],计算机系统应用,2006,3,90-93
[11]朱景,李宗斌,高新勤.基于多色集合的工作流建模及路径求取算法[J],西安交通大学学报,2006,9(3),348-353
[12]F.Castal,P.Grefen,B.Penrici et al..WIDE Workflow Model Architecture.T ech.Report,Dept.of C.E,Twente University,and 1996
[13]Wil van der Aalst and Kees Max van Hee.Workflow Management:Models,Methods and Systems.The MIT Press Cambridge,Massachusetts London,England.2002
[14]W.M.P.van der Aalst,J.Desel and A.Oberweis,editors.Business Process Management:Models,Techniques and Empirical Studies,volume 1806 of Lecture Notes in Computer Science.Springer-Verlag.Berlin,2000
[15]W.M.P.van der Aalst and S.Jablonski editors.Flexible Workflow Technology Driving the Networked Economy,Special Issue of the International Journal of Computer Systems,Science,and Engineering,2000,15(5)
[16]W.M.P.van der Aalst,A.J.M.M.Weijters and L.Marnster.Workflow mining:which processes can be rediscovered,Working Paper WP74,Beta Research School for Operations Management and Logistic,Eindhoven Technical University,2002:1-25
[17]P.C.Attie and N.A.Lynch,Dynamic input/output automata:a formal model for dynamic systems,Prodeedings of CONCUR 01,12th International Conference on Concurrency Theory.Aug.2001,LNCS,Springer-Verlag.Aalborg,Denmark
[18]Paul C.Attie.Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs.The 6th International Conference on Verification,Model Checking,and Abstract Interpretation(VMCAI 2005) Pads,France
[19]The CIMOSA Business Modelling Process.Computer inIndustry.Martin Z elm,Francois R 1995
[20]徐宝文,周毓明,卢红敏编著.UML与软件建模[M].北京:清华大学出版社,2006
[21]沈美,刘同义,于翔,丁香乾.基于高级Petri网的工作流建模研究与仿真分析[J],计算机工程与应用,2006-32:
[22]万和平,王明哲.层次工作流Petri网建模与分析[J],计算机工程与应用,2005(15)
[23]杨雯,刘厚泉.基于Petri网的工作流模型的研究[J],计算机工程与设计,2007,17(07)
[24]唐达,徐超,杨晓丽.工作流建模中时态逻辑的研究与应用[J],计算机集成制造系统---CIMS:2004(04),388-394
[25]王远,范玉顺.基于时序逻辑的工作流建模与分析方法[J],高技术通讯2006,16(02)
[26]李毅.产品协同设计工作流MCM/CLM建模技术研究及仿真[D],武汉:武汉理工大学,2005
[27]汪文元,沙基昌,谭东风.基于概念模型工程的工作流建模研究[J],计算机工程与科学,2006,28(1)
[28]方进,王铁成,石志宽,谢俊元.基于UML的工作流建模[J].计算机工程与设计.2004,9 1572-1575
[29]曾清华,李青.基于扩展的UML活动图的质量工作流建模[J],航空精密制造技术,2005,2
[30]管红杰,孟凡荣,孙晋非.基于UML的工作流管理系统建模的应用研究[J],计算机工程与设计,2006,(01),99-103
[31]江敬尧,张自慧,仲兆满.基于UML的工作流建模研究[J].太原师范学院学报(自然科学版),2008,6
[32]谢子松,武友新,牛德雄.基于UML的工作流建模的研究与应用[J],计算机系统应用2005,2
[33]张秋余,王雪等.基于UML的工作流建模的研究[J],兰州理工大学学报,2006,20(04),932-935
[34]邹文玲,华凡,刘希玉.基于UML的工作流建模研究与应用[J],信息技术与信息化,2006,5,74-76
[35]H.M.W.Verberk,T.Basten and W.M.R van der Aalst.Diagnosing workflow Processes using Woflan[J].The Computer Jounral,44(4):246-279,2001
[36]P.Muth,D.wodtke,J.Wotke,J.Weissenefls,G.Weikun,and A.Kotz-Dittrieh.Enteprrize-wide wokrflow management based on state and activity eharts[J].NATO/ASI Workflow Management Systems and Interoperability.Springer,1998
[37]C.Karamanolis L,D.Giannakopoulou,J.Magee,S.M.Wheater.Model Checking of Workflow,Schemas[J].The Fourth Intemational Enteprrise Distributed Object Computing Conefernee,SePtember25-28,2000
[38]陈火旺,王戟,董威.高可信软件工程技术[J].电子学报,2003,31(12A)
[39]Vitus S.W.Lan,Julian Padget.Symbolic Model Checking of UML s tatechart Dragrams with an Integrated Approach[C].Proc.11th IEEE International Conference and workshop on the Engineering of Computer-Based systems,(ECBS'04),Brno,Czech Repubic,2004
[40]崔萌.UML模型转换和验证的研究[D].南京:南京大学,2003
[41]董威.面向UML的模型检验研究[D].长沙:国防科技大学,2002
[42]燕吴.UML建模的形式化研究[D].兰州:兰州大学,2006
[43]M.Farid,G.Patrice,B.Mourad.Verifying UML Diagrams with Model checking:A Rewriting Logic Based Approach[C].Proc 7th Quality software International Conference,Portland,Oregon,2007,11-12:356-362
[44]T.Clark,Type checking UML static Models[M].Lectare Notes in Computer Science 1723,Springer-Verlag,Berlin 1999,503-510
[45]董威,王戟,郑延平,齐治昌.UML状态机的模型检验方法[J].计算机工程与科学,2001,23(06)
[46]王璐珍,董威,陈火旺.UML顺序图的自动验证[J].计算机工程与应用,2003,29.80-83
[47]汪文元,沙基昌,谭东风.基于网和活动图工作流建模比较[J].系统仿真学报,2006,02
[48]孙莹.Petri网和UML在建模过程中的转换机制研究[D].大连:大连海事 大学,2008
[49]朱彩霞.浅谈形式语义研究的意义和现状[J].科技资讯,2000,(47):195
[50]赖明志,尤晋元.从UML状态图到PVS规范的自动转换、验证[J].电子学报,2002,30(12A)
[51]单卓为.基于SPIN的UML模型验证技术的研究[D].西安:西北大学,2008,3
[52]汪文元,沙基昌.基于UML活动图化简方法的工作流模型校核研究[J].计算机工程,2006,32(15)
[53]M.Elaasar,L.Briand.An Overview of UML Consistency Management.Technical Report SCE-04-18,Department of Systems and Computer Engineering,Ottawa,Canada.August24,2004
[54]Bas Graaf and Arie van Deursen.Model Driven Consitency Checking of Behavioral Specification.In:Fourth Intnationall Workshop on Model-Based Methodologies for Pervasive and Embedded Software(MOMPES'07),Braga,Portugal,IEEE Computer Press,2007,115-126
[55]Vitus S,W.Lam and Julian Padget.Consistency Checking of Sequence Diagramsand Statechart Diagrams Using theπ-Calculus.Springer-Verlag,2005,LNCS 3771,347-365.
[56]P.Inverardi,H.Muccini,and P.Pelliccione.Checking consistency between architectural models using SPIN.In Proc.of STRAW'01,Toronto,Canada,2001
[57]G.Engels,J.M.K(A|¨)uster,L.Groenewegen,and R.Heckel.Am ethodology for specifying and analyzing consistency of object-oriented behavioral models.Proceedings of the 8th European Software Engineering Conference(ESEC),ACM Press,2001.186-195
[58]G.Engels,J.Hausmann,R.Heckel,and S.Sauer.Testing the consistency of dynamic UML diagrams.In Proc.Sixth International Conference on Integrated Design and Process Technology(IDPT 2002),June 2002.Pasadena,CA,USA
[59]B.Selic.Using UML for modeling complex real-time systems.Springer-Verlag,1999,LNCS 1474,250-262
[60]J.M.K(u|¨)ster,J.Stroop.Consistent Design of embedded Real-Time Systems with UML-RT.In:4th International Symposium on Object-Oriented Real-Time Distributed Computing(ISORC'01),Magdeburg,Germany,IEEE Computer Society Press,2001,31-40
[61]T.Firley,M.Huhn,K.Diethers et al.Timed Sequence Diagrams and Tool-Based Analysis-A Case Study.Springer-Verlag,1999,LNCS1723,645-660
[62]A.Knapp,S.Merz,C.Rauh.Model Checking Timed UML State Machines and Collaborations.Springer-Verlag,2002,LNCS 2469,395-416
[63]Behrmann G,David A,Larsen K G.A tutorial on UPPAAL.http://www.it.se /research/group/darts/papers/texts/new-tutorial.pdf,2004-11-07
[64]Behrmann.G,David A,Hakansson J et al.UPPAAL4.0.In:3rd International Conference on the Quantitative Evaluation of Systems(QESY'06),University of California,USA,IEEE Computer Society Press,2006,125-126
[65]Timm Sch(a|¨)fer,Alexander Knapp,and Stephan Merz.Model Checking UML StateMachines and Collaborations.Proc.Wsh.Software Model Checking,Elect.Notes Theo.Comp.Sci.,55(3),2001.1-13
[66]J.M.K(A|¨)uster and J.Stehr.Towards Explicit Behavioral Consistency Concepts in theUML.In Proceedings of the 2nd International Workshop on Scenarios and State Machines:Models,Algorithms and Tools,2003
[67]W.Damm and D.Harel.Breathing life into message sequence charts.Formal Methods in System Design,2001(19),45-80
[68]Boris Litvak,Behavioral Consistency Validation of UML diagrams.Proceedings of the 1st Proc.of the First International Conference on Software Engineering and Formal Methods(SEFM'03),(2003).118-125
[69]Li Xuandong,Lilius,J..Checking Compositions of UML Sequence Diagrams forTiming Inconsistency.In:7th Asia-Pacific Software Engineer Conference (APSEC2000),Singapore,IEEE Computer Society Press,2000,154-161
[70]Li Xuandong,Zhao Jianhua,Gong Jiayu.Verifying Compositional Designs for Scenario-Based Timing Specifications.In:Proceedings of the 7th IEEEInternational Symposium on Object-Oriented Real-Time Distributed Computing(ISORC2004),Vienna,Austria,IEEE Computer Society Press,2004,253-256
[71]王洪媛.顺序图与状态图的一致性问题的研究[D],吉林:吉林大学,2007
[72]凌云翔,马满好,袁卫卫等著.作战模型与模拟[M].长沙:国防科技大学出版社。2006,10
[73]Coloel Sorah Smith.Accelerating Lean in DoD MRO,Estaishing Context and Defining the Challenge[EB],http://www.osd.atl.mil/lean forum intr.ppt,Apr.15,2004
[74]美军装备精益维修案例分析.http://blog.sina.com.cn羌人,2007,04-22
[75]张瑾,赵捧未.基于UML模型的装备维修信息管理系统分析与设计[J],情报科学.2007,25(4)575-578
[76]孙云,张东升,王日恒,孙万国.基于UML的装备保障指挥控制工作流模型[J].装甲兵工程学院学报,2008,1
[77]军事装备学[M].北京:国防大学出版社2000,9
[78]王鲁滨等编著.现代信息管理[M].北京:经济管理出版社,2005
[79]沈建明.中国国防项目管理知识体系[M].北京:国防工业出版社,2006,
[80]周健临.管理学教程[M].上海:上海财经大学出版社,2003
[81]陈庆华.装备运筹学[M].北京:国防工业出版社,2005
[82]Craig Dewalt."Bussiness process Modeling with UML"[EB/OL].http://www.Umlchina.com
[83]Nasser Kettani.Unilog "uses object Technology and Business Modeling for Their astomer success"[EB/OL],http://www.rational.com 2000
[84]张立厚,莫赞,张延林,陶雷.管理信息系统:开发与管理[M].北京:清华大学出版社.2008
[85]蔡敏,徐慧慧,黄炳秋编著.UML基础与Rose建模案例[M].北京:人民邮电出版社,2006
[86]曾强聪,赵歆,王四春.基于工作流的高校综合信息系统的分析与设计[J],科学技术与工程,2006,19(6):3097-3101
[87]法,Claude Girault;德R(u|¨)diger Valk,著;王生原,余鹏,霍金键等译.袁崇义审核.系统工程Petri网--建模、验证与应用指南[M].电子工业出版社,2005
[88]张文静.基于UML和形式化方法的构件体系结构研究与应用[D].北京:华北电力大学,2005
[89]张红军.一类对象Petri网建模与验证方法研究[D].郑州:郑州大学,2006
[90]李建强,范玉顺.一种工作流模型的性能分析方法[J].计算机学报,2003,26(05):513-523
[91]古天龙,蔡国永.网络协议的形式化分析与设计[M].北京:电子工业出版社,2003,277-279
[92]计算机研究生开放课程《自动模型检测-SPIN的建模语言Promela》http://210.40.7.188/E'ojc/MXJC/SPIN/000/001.asp
[93]陈卉,窦万峰.UML状态图和顺序图的一致性检验[J],计算机工程,2008,9,62-64
[94]陈卉.UML顺序图和状态图的形式化研究[D].南京:南京师范大学,2008
[95]刘晓建,李战怀.基于扩展层次自动机的UML状态图完备性和一致性检验[J],微电子学与计算机,2008.139-44
[96]刘传会.基于UML2.0的实时软件动态行为模型一致性验证[D].兰州:兰州大学,2008,4
[97]董威,王戟,齐治昌.UMLstmechags的模型验证方法[J],软件学报,2003, 14(03) 750-755
[98]An Overview to the XMI-XML Metadata Interchanger Specification[S],http//cgi.omg.org/news/pr99/xmi_overview.html.
[99]R Alur,M Yann akakis.Model checking of message sequene charts[C].In:CONCUR99,VOLUMN 1664 of Lecture Notes in Computer Science,1999
[100]Zhao Xiangpeng,Long Quan,Qiu Zongyan.Model Checking Dynamic UML Consistency[C]//Proceedings of the 8th Int'1 Conference on Formal Engineering Methods.Macao,China:[s.n.],2006
[101]谢洪萍.基于UML的工作流模型自动分析验证研究[D].广州:华南师范大学,2005
[2]Davenport T.H,Short J.E.The new industrial engineering:information technology and business Process redesign[J].Sloan management Review,1990,31(4):11-27
[3]张传芹.基于工作流的业务过程建模及应用研究[D].南京:东南大学,2003,4
[4]在新的起点上再创辉煌[J].通用装备保障.北京:通用装备保障编辑部,2008,6
[5]花兴来,刘庆华.装备管理工程[M].北京:国防工业出版社,2202,7
[6]李振英,卢华明,戴丽萍.管理信息系统与工作流系统的结合[J].北京:机械工业学院学报,2006,21(9)
[7]范玉顺,吴澄.工作流管理技术基础[M].北京:清华大学出版社,2001
[8]荷兰Wil Van der Aalst & Kees Van Hee著;王建民,闻立杰等译.工作流管理[M].北京:清华大学出版社,2004,1
[9]范玉顺,吴澄.工作流管理技术研究与产品现状及发展趋势[J].计算机集成制造系统-CIMS,2000,6(1):1-7
[10]蒋国银,董利红.工作流过程建模理论综述[J],计算机系统应用,2006,3,90-93
[11]朱景,李宗斌,高新勤.基于多色集合的工作流建模及路径求取算法[J],西安交通大学学报,2006,9(3),348-353
[12]F.Castal,P.Grefen,B.Penrici et al..WIDE Workflow Model Architecture.T ech.Report,Dept.of C.E,Twente University,and 1996
[13]Wil van der Aalst and Kees Max van Hee.Workflow Management:Models,Methods and Systems.The MIT Press Cambridge,Massachusetts London,England.2002
[14]W.M.P.van der Aalst,J.Desel and A.Oberweis,editors.Business Process Management:Models,Techniques and Empirical Studies,volume 1806 of Lecture Notes in Computer Science.Springer-Verlag.Berlin,2000
[15]W.M.P.van der Aalst and S.Jablonski editors.Flexible Workflow Technology Driving the Networked Economy,Special Issue of the International Journal of Computer Systems,Science,and Engineering,2000,15(5)
[16]W.M.P.van der Aalst,A.J.M.M.Weijters and L.Marnster.Workflow mining:which processes can be rediscovered,Working Paper WP74,Beta Research School for Operations Management and Logistic,Eindhoven Technical University,2002:1-25
[17]P.C.Attie and N.A.Lynch,Dynamic input/output automata:a formal model for dynamic systems,Prodeedings of CONCUR 01,12th International Conference on Concurrency Theory.Aug.2001,LNCS,Springer-Verlag.Aalborg,Denmark
[18]Paul C.Attie.Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs.The 6th International Conference on Verification,Model Checking,and Abstract Interpretation(VMCAI 2005) Pads,France
[19]The CIMOSA Business Modelling Process.Computer inIndustry.Martin Z elm,Francois R 1995
[20]徐宝文,周毓明,卢红敏编著.UML与软件建模[M].北京:清华大学出版社,2006
[21]沈美,刘同义,于翔,丁香乾.基于高级Petri网的工作流建模研究与仿真分析[J],计算机工程与应用,2006-32:
[22]万和平,王明哲.层次工作流Petri网建模与分析[J],计算机工程与应用,2005(15)
[23]杨雯,刘厚泉.基于Petri网的工作流模型的研究[J],计算机工程与设计,2007,17(07)
[24]唐达,徐超,杨晓丽.工作流建模中时态逻辑的研究与应用[J],计算机集成制造系统---CIMS:2004(04),388-394
[25]王远,范玉顺.基于时序逻辑的工作流建模与分析方法[J],高技术通讯2006,16(02)
[26]李毅.产品协同设计工作流MCM/CLM建模技术研究及仿真[D],武汉:武汉理工大学,2005
[27]汪文元,沙基昌,谭东风.基于概念模型工程的工作流建模研究[J],计算机工程与科学,2006,28(1)
[28]方进,王铁成,石志宽,谢俊元.基于UML的工作流建模[J].计算机工程与设计.2004,9 1572-1575
[29]曾清华,李青.基于扩展的UML活动图的质量工作流建模[J],航空精密制造技术,2005,2
[30]管红杰,孟凡荣,孙晋非.基于UML的工作流管理系统建模的应用研究[J],计算机工程与设计,2006,(01),99-103
[31]江敬尧,张自慧,仲兆满.基于UML的工作流建模研究[J].太原师范学院学报(自然科学版),2008,6
[32]谢子松,武友新,牛德雄.基于UML的工作流建模的研究与应用[J],计算机系统应用2005,2
[33]张秋余,王雪等.基于UML的工作流建模的研究[J],兰州理工大学学报,2006,20(04),932-935
[34]邹文玲,华凡,刘希玉.基于UML的工作流建模研究与应用[J],信息技术与信息化,2006,5,74-76
[35]H.M.W.Verberk,T.Basten and W.M.R van der Aalst.Diagnosing workflow Processes using Woflan[J].The Computer Jounral,44(4):246-279,2001
[36]P.Muth,D.wodtke,J.Wotke,J.Weissenefls,G.Weikun,and A.Kotz-Dittrieh.Enteprrize-wide wokrflow management based on state and activity eharts[J].NATO/ASI Workflow Management Systems and Interoperability.Springer,1998
[37]C.Karamanolis L,D.Giannakopoulou,J.Magee,S.M.Wheater.Model Checking of Workflow,Schemas[J].The Fourth Intemational Enteprrise Distributed Object Computing Conefernee,SePtember25-28,2000
[38]陈火旺,王戟,董威.高可信软件工程技术[J].电子学报,2003,31(12A)
[39]Vitus S.W.Lan,Julian Padget.Symbolic Model Checking of UML s tatechart Dragrams with an Integrated Approach[C].Proc.11th IEEE International Conference and workshop on the Engineering of Computer-Based systems,(ECBS'04),Brno,Czech Repubic,2004
[40]崔萌.UML模型转换和验证的研究[D].南京:南京大学,2003
[41]董威.面向UML的模型检验研究[D].长沙:国防科技大学,2002
[42]燕吴.UML建模的形式化研究[D].兰州:兰州大学,2006
[43]M.Farid,G.Patrice,B.Mourad.Verifying UML Diagrams with Model checking:A Rewriting Logic Based Approach[C].Proc 7th Quality software International Conference,Portland,Oregon,2007,11-12:356-362
[44]T.Clark,Type checking UML static Models[M].Lectare Notes in Computer Science 1723,Springer-Verlag,Berlin 1999,503-510
[45]董威,王戟,郑延平,齐治昌.UML状态机的模型检验方法[J].计算机工程与科学,2001,23(06)
[46]王璐珍,董威,陈火旺.UML顺序图的自动验证[J].计算机工程与应用,2003,29.80-83
[47]汪文元,沙基昌,谭东风.基于网和活动图工作流建模比较[J].系统仿真学报,2006,02
[48]孙莹.Petri网和UML在建模过程中的转换机制研究[D].大连:大连海事 大学,2008
[49]朱彩霞.浅谈形式语义研究的意义和现状[J].科技资讯,2000,(47):195
[50]赖明志,尤晋元.从UML状态图到PVS规范的自动转换、验证[J].电子学报,2002,30(12A)
[51]单卓为.基于SPIN的UML模型验证技术的研究[D].西安:西北大学,2008,3
[52]汪文元,沙基昌.基于UML活动图化简方法的工作流模型校核研究[J].计算机工程,2006,32(15)
[53]M.Elaasar,L.Briand.An Overview of UML Consistency Management.Technical Report SCE-04-18,Department of Systems and Computer Engineering,Ottawa,Canada.August24,2004
[54]Bas Graaf and Arie van Deursen.Model Driven Consitency Checking of Behavioral Specification.In:Fourth Intnationall Workshop on Model-Based Methodologies for Pervasive and Embedded Software(MOMPES'07),Braga,Portugal,IEEE Computer Press,2007,115-126
[55]Vitus S,W.Lam and Julian Padget.Consistency Checking of Sequence Diagramsand Statechart Diagrams Using theπ-Calculus.Springer-Verlag,2005,LNCS 3771,347-365.
[56]P.Inverardi,H.Muccini,and P.Pelliccione.Checking consistency between architectural models using SPIN.In Proc.of STRAW'01,Toronto,Canada,2001
[57]G.Engels,J.M.K(A|¨)uster,L.Groenewegen,and R.Heckel.Am ethodology for specifying and analyzing consistency of object-oriented behavioral models.Proceedings of the 8th European Software Engineering Conference(ESEC),ACM Press,2001.186-195
[58]G.Engels,J.Hausmann,R.Heckel,and S.Sauer.Testing the consistency of dynamic UML diagrams.In Proc.Sixth International Conference on Integrated Design and Process Technology(IDPT 2002),June 2002.Pasadena,CA,USA
[59]B.Selic.Using UML for modeling complex real-time systems.Springer-Verlag,1999,LNCS 1474,250-262
[60]J.M.K(u|¨)ster,J.Stroop.Consistent Design of embedded Real-Time Systems with UML-RT.In:4th International Symposium on Object-Oriented Real-Time Distributed Computing(ISORC'01),Magdeburg,Germany,IEEE Computer Society Press,2001,31-40
[61]T.Firley,M.Huhn,K.Diethers et al.Timed Sequence Diagrams and Tool-Based Analysis-A Case Study.Springer-Verlag,1999,LNCS1723,645-660
[62]A.Knapp,S.Merz,C.Rauh.Model Checking Timed UML State Machines and Collaborations.Springer-Verlag,2002,LNCS 2469,395-416
[63]Behrmann G,David A,Larsen K G.A tutorial on UPPAAL.http://www.it.se /research/group/darts/papers/texts/new-tutorial.pdf,2004-11-07
[64]Behrmann.G,David A,Hakansson J et al.UPPAAL4.0.In:3rd International Conference on the Quantitative Evaluation of Systems(QESY'06),University of California,USA,IEEE Computer Society Press,2006,125-126
[65]Timm Sch(a|¨)fer,Alexander Knapp,and Stephan Merz.Model Checking UML StateMachines and Collaborations.Proc.Wsh.Software Model Checking,Elect.Notes Theo.Comp.Sci.,55(3),2001.1-13
[66]J.M.K(A|¨)uster and J.Stehr.Towards Explicit Behavioral Consistency Concepts in theUML.In Proceedings of the 2nd International Workshop on Scenarios and State Machines:Models,Algorithms and Tools,2003
[67]W.Damm and D.Harel.Breathing life into message sequence charts.Formal Methods in System Design,2001(19),45-80
[68]Boris Litvak,Behavioral Consistency Validation of UML diagrams.Proceedings of the 1st Proc.of the First International Conference on Software Engineering and Formal Methods(SEFM'03),(2003).118-125
[69]Li Xuandong,Lilius,J..Checking Compositions of UML Sequence Diagrams forTiming Inconsistency.In:7th Asia-Pacific Software Engineer Conference (APSEC2000),Singapore,IEEE Computer Society Press,2000,154-161
[70]Li Xuandong,Zhao Jianhua,Gong Jiayu.Verifying Compositional Designs for Scenario-Based Timing Specifications.In:Proceedings of the 7th IEEEInternational Symposium on Object-Oriented Real-Time Distributed Computing(ISORC2004),Vienna,Austria,IEEE Computer Society Press,2004,253-256
[71]王洪媛.顺序图与状态图的一致性问题的研究[D],吉林:吉林大学,2007
[72]凌云翔,马满好,袁卫卫等著.作战模型与模拟[M].长沙:国防科技大学出版社。2006,10
[73]Coloel Sorah Smith.Accelerating Lean in DoD MRO,Estaishing Context and Defining the Challenge[EB],http://www.osd.atl.mil/lean forum intr.ppt,Apr.15,2004
[74]美军装备精益维修案例分析.http://blog.sina.com.cn羌人,2007,04-22
[75]张瑾,赵捧未.基于UML模型的装备维修信息管理系统分析与设计[J],情报科学.2007,25(4)575-578
[76]孙云,张东升,王日恒,孙万国.基于UML的装备保障指挥控制工作流模型[J].装甲兵工程学院学报,2008,1
[77]军事装备学[M].北京:国防大学出版社2000,9
[78]王鲁滨等编著.现代信息管理[M].北京:经济管理出版社,2005
[79]沈建明.中国国防项目管理知识体系[M].北京:国防工业出版社,2006,
[80]周健临.管理学教程[M].上海:上海财经大学出版社,2003
[81]陈庆华.装备运筹学[M].北京:国防工业出版社,2005
[82]Craig Dewalt."Bussiness process Modeling with UML"[EB/OL].http://www.Umlchina.com
[83]Nasser Kettani.Unilog "uses object Technology and Business Modeling for Their astomer success"[EB/OL],http://www.rational.com 2000
[84]张立厚,莫赞,张延林,陶雷.管理信息系统:开发与管理[M].北京:清华大学出版社.2008
[85]蔡敏,徐慧慧,黄炳秋编著.UML基础与Rose建模案例[M].北京:人民邮电出版社,2006
[86]曾强聪,赵歆,王四春.基于工作流的高校综合信息系统的分析与设计[J],科学技术与工程,2006,19(6):3097-3101
[87]法,Claude Girault;德R(u|¨)diger Valk,著;王生原,余鹏,霍金键等译.袁崇义审核.系统工程Petri网--建模、验证与应用指南[M].电子工业出版社,2005
[88]张文静.基于UML和形式化方法的构件体系结构研究与应用[D].北京:华北电力大学,2005
[89]张红军.一类对象Petri网建模与验证方法研究[D].郑州:郑州大学,2006
[90]李建强,范玉顺.一种工作流模型的性能分析方法[J].计算机学报,2003,26(05):513-523
[91]古天龙,蔡国永.网络协议的形式化分析与设计[M].北京:电子工业出版社,2003,277-279
[92]计算机研究生开放课程《自动模型检测-SPIN的建模语言Promela》http://210.40.7.188/E'ojc/MXJC/SPIN/000/001.asp
[93]陈卉,窦万峰.UML状态图和顺序图的一致性检验[J],计算机工程,2008,9,62-64
[94]陈卉.UML顺序图和状态图的形式化研究[D].南京:南京师范大学,2008
[95]刘晓建,李战怀.基于扩展层次自动机的UML状态图完备性和一致性检验[J],微电子学与计算机,2008.139-44
[96]刘传会.基于UML2.0的实时软件动态行为模型一致性验证[D].兰州:兰州大学,2008,4
[97]董威,王戟,齐治昌.UMLstmechags的模型验证方法[J],软件学报,2003, 14(03) 750-755
[98]An Overview to the XMI-XML Metadata Interchanger Specification[S],http//cgi.omg.org/news/pr99/xmi_overview.html.
[99]R Alur,M Yann akakis.Model checking of message sequene charts[C].In:CONCUR99,VOLUMN 1664 of Lecture Notes in Computer Science,1999
[100]Zhao Xiangpeng,Long Quan,Qiu Zongyan.Model Checking Dynamic UML Consistency[C]//Proceedings of the 8th Int'1 Conference on Formal Engineering Methods.Macao,China:[s.n.],2006
[101]谢洪萍.基于UML的工作流模型自动分析验证研究[D].广州:华南师范大学,2005