软件工程中的形式化方法研究论文

教师队伍情况 经过近10年的课程建设，围绕本课程，形成了由广西首批教学团队负责人、学校示范教授、教学名师董荣胜具体负责，由全国模范教师、广西教学名师古天龙教授指导，拥有学校“十佳师德”标兵称号的，多次获得国家和省部级有关教学奖，发表多篇（部）在国内较有影响教学论著、结构合理、年轻而又有富有朝气的师资队伍。 一、课程负责人董荣胜，男，广西高等学校教学名师，桂林电子科技大学计算思维及应用研究室主任、教授、硕士生导师。二、教学指导及专题讲座古天龙，男，博士，桂林电子科技大学副校长、教授、博士生导师。三、主讲教师钟艳如，女，硕士，桂林电子科技大学计算机与控制学院副院长，计算思维及应用研究室教授、硕士生导师。陈光喜，男，博士，桂林电子科技大学现代教育技术中心主任、副教授、硕士生导师。赵岭忠，男，博士，桂林电子科技大学计算思维及应用研究室副教授、硕士生导师。常 亮，男，博士，桂林电子科技大学计算思维及应用研究室副教授、硕士生导师。李凤英，女，硕士，桂林电子科技大学计算思维及应用研究室讲师。课程负责人董荣胜教授 董荣胜，男，广西高等学校教学名师，桂林电子科技大学计算思维及应用研究室主任、教授、硕士研究生导师。1989年7月毕业于中国地质大学计算机科学系，现为全国高等学校计算机教育研究会理事、中国计算机学会教育专业委员会委员、广西计算机学会理事、广西首批区级教学团队负责人、桂林电子科技大学教学指导委员会委员、学校示范教授、教学名师。研究方向：网络安全协议、形式化技术、计算思维与计算机方法论。承担了国家八五攻关项目、总装备部项目、国家863计划项目、国家自然科学基金、国防预研项目、广西科学基金等国家和省部级科研项目10余项，是计算学科认知理论——计算机科学与技术方法论的构建者和倡导者，在国内外重要学术刊物和会议发表学术论文80余篇，出版著作型教材2部，以第一作者撰写的论文和著作分别被他人引用160多次，主要成果被美国计算学科教程（CC2001）和《中国计算机科学与技术学科教程2002》采用，撰写的教材《计算机科学导论——思想与方法》（高等教育出版社，2007年9月出版）被北京大学国家级精品课程“计算概论”列为推荐教材的首位、撰写的《计算机科学与技术方法论》（人民邮电出版社，2002年9月出版）与《计算机科学导论——思想与方法》分别被华中科技大学等国内数十所高校选为教材，主持和参与的教改项目分别获广西优秀教学成果奖一等奖2次、三等奖2次，撰写的教材分别获广西优秀教材一等奖1次、广西社会科学优秀成果三等奖1次。主讲教师古天龙教授 古天龙（教授/博导/博士）生于山西、芮城，分别于、、在太原理工大学、西安电子科技大学、浙江大学获工学学士、硕士、博士学位。至在澳大利亚CURTIN理工大学、MURDOCH大学进行博士后研究。1998年破格晋升教授，至今为西安电子科技大学博士生导师。至今任桂林电子科技大学副校长。现为IEEE高级会员、ACM会员、教育部高等学校计算机科学与技术教学指导委员会软件工程专业分会委员、中国计算机学会Petri网专委会委员、中国计算机学会计算机工程与工艺专委会委员、中国人工智能学会知识工程与分布式智能专委会委员、广西计算机学会副理事长、《计算机科学》编委。多年来一直从事计算机科学与技术和控制科学与工程交叉学科的教学和科研工作，主要研究领域为：软件工程与形式化方法；知识工程与符号计算；嵌入式系统；传感器网络与协议工程；离散事件/混杂系统等。近年来主持国家863计划项目、国家自然科学基金、国防预研重点项目、国防预研基金、中澳国际合作项目、教育部留学回国人员基金等20余项。出版学术著作/教材《软件开发的形式化方法》（高等教育出版社，2005）、《网络协议的形式化分析与设计》（电子工业出版社，2003）、《软件工程》（电子工业出版社，2004）、《计算机科学与技术方法论》（人民邮电出版社，2002）、《离散数学》（电子工业出版社，2008）等5部，在国内外重要学术刊物和会议发表学术论文130篇（其中EI、SCI收录51篇）。入选“国家百千万人才工程”(2004)、“广西十百千人才工程”（2000）、“广西高校跨世纪中青年学科带头人”（1996），并荣获全国模范教师（1998）、国务院政府特殊津贴专家（2004）、广西优秀专家（2007）、广西优秀留学回国人员（2006）、广西教学名师（2008）、电子工业部优秀科技青年（1996）、电子工业系统优秀教师（1997）、广西高校科技进步二等奖（1998）、广西优秀教材一等奖（2006）、广西优秀教材一等奖（2003）、广西优秀教学成果一等奖（2004）、广西社会科学优秀成果三等奖（2004）等。主讲教师钟艳如教授 钟艳如（教授/硕导） 生于江西、宜春，分别于、于桂林电子科技大学获工学学士、硕士学位。晋升教授。现任全国高等学校计算机教育研究会计算机网络教育分会理事，广西计算机学会会员，桂林电子科技大学计算机与控制学院副院长。多年来一直从事计算机学科科学与工程交叉学科的教学和科研工作。主要研究领域为：知识工程与符号计算、计算机辅助精度设计、新一代GPS标准体系的理论等。共承担和完成科研项目12项，其中包括，主持区自然科学基金(2007年)、区教育厅项目(2004年)、横向课题(2005年)和校科研课题(2003年)各1项，参加国家自然科学基金排名第二(2006年和2009年)2项和排名第四(2003年) 1项，参加（排名第二,2004年）教育部科学技术研究重大项目子课题1项，参加（排名第二，2006年）区自然科学基金1项，参加（排名第二，2004年）教育部科学技术研究重点项目1项，参加区教育厅科研项目（排名第二，2002年）和（排名第三，2006年）各1项。共承担和完成教改项目6项：主持广西教育科学“十五”规划立项课题1项，参加区高等学校精品课程排名2项（排均为名第三），校级教改项目3项（其中两项排名第一，一项排名第二）。共发表论文40多篇，其中，国际四大索引（SCI、EI、ISR、ISTP）收录期刊15篇。荣获广西优秀教学成果一等奖(“计算机科学与技术方法论的建立及其教学实践”，2004，第四)、、《多媒体技术》网络课程获得广西教育厅多媒体课件优秀奖（2004，负责人）、曾出席中国共产党广西壮族自治区第八次代表大会，获得十佳师德标兵（2008）等。主讲教师陈光喜副教授 陈光喜（副教授/博士），男，汉族，1971年生。1997年7月复旦大学数学研究所计算数学专业硕士毕业；2002年7月中国科学院成都计算所计算机软件与理论专业博士毕业。1997年7月至2003年8月中国科学院成都计算所自动推理实验室助理研究员；2003年8月至今，桂林电子科技大学副教授。2005年6月起任桂林电子科技大学现代教育技术中心主任。从事计算机软件与理论、应用数学专业的教学与科研工作。广西教育技术协会常务理事。近3年来参加国家自然基金项目2项，主持广西教育厅科研和教改项目6项，其它科研项目8项；发表科研论文24篇,其中EI检索4篇；发表教学论文12篇；主编教材1部。获桂林市科技进步三等奖1项,全国多媒体课件大赛一等奖1项, 全国多媒体课件大赛三等奖1项，广西教育教学软件大赛一等奖2项。主讲教师赵岭忠副教授 赵岭忠(副教授/博士)，生于河南、南阳。分别于、在桂林电子科技大学、西安电子科技大学获工学硕士、博士学位. 近年来主持和参与国家自然科学基金、广西自然科学基金等项目10余项。涉及领域包括：复杂生产过程的符号调度、面向对象分布式实时系统的建模与任务调度、安全协议分析及模型检验等. 参与计算机科学与技术方法论的研究，并于2005年获广西区高等教育教学成果一等奖. 在《Software Quality Journal》、《计算机研究与发展》、《计算机科学》、《计算机集成制造系统》、《通信学报》、《计算机工程》等国内核心期刊及“APLAS’07”、“TASE’07”、“PRICAI’06”、“AI’06”、“SEKE’06”等重要的软件工程和人工智能国际学术会议上发表和录用论文近40篇. 目前的研究兴趣包括：逻辑程序在人工智能和软件验证领域的应用，抽象解释理论及其在逻辑程序的分析和验证、软件安全领域的应用,符号计算等。主讲教师常亮副教授 常亮(副教授/博士)，1980年6月生，2008年7月毕业于中国科学院计算技术研究所，获工学博士学位。主要研究方向为行动理论、描述逻辑、语义Web服务、智能主体、以及形式化方法。作为主要成员先后参与或完成了1项973项目子项目、1项国家863项目、2项国家自然科学基金项目。在《计算机学报》、《软件学报》、《计算机研究与发展》、《Service Oriented Computing and Applications》等国内外期刊以及“DL’07”、“KSEM’07”、“PRICAI’08”、“ICWS’08”等重要国际学术会议上发表论文20余篇，其中被EI收录11篇。 《计算机科学导论》课程教学大纲 课程类别：专业基础必修课 课程代码：总 学 时：48学时（其中，理论课32学时，实验课16学时） 学分：3适用专业：计算机科学与技术、软件工程、网络工程、信息安全、信息系统与信息管理、数字媒体、教育技术学等先修课程：无一、课程的地位、性质和任务本课程是计算机科学与技术专业学生入学学习的第一门专业必修课，它构建在计算学科认知模型的基础上，以计算思维能力的培养为核心，从学科思想与方法层面对计算学科进行导引。本课程来源于ACM教育委员会对“整个计算学科综述性导引”（计算机导论）课程构建的要求，即用严密的方式将学生引入计算学科各个富有挑战性的领域之中。本课程为学生正确认知计算学科提供方法，为今后深入学习计算机课程作铺垫。二、课程教学的基本要求本课程要求学生了解计算学科专业名称的演变，学科的描述、培养侧重点，学科各专业方向的知识体与核心课程，“计算机导论”课程的构建，了解计算学科的历史，计算学科的基本问题；计算学科中的抽象、理论和设计三个过程及其内在联系；了解计算学科各主领域的基本内容及其相应的课程设置、计算学科中的核心概念、数学方法、系统科学方法、社会和职业问题、学科若干问题、学科教育发展与展望等内容。三、教学内容与学时分配1．绪论（2学时）计算学科的定义；计算学科的根本问题；计算学科专业名称的演变；分支学科及其培养侧重点；计算机科学、计算机工程、软件工程和信息技术等4个主要分支学科的知识体和核心课程；最后，“计算机导论”课程的构建问题；计算学科认知模型——计算学科二维定义矩阵；计算学科若干问题的介绍。2．计算学科的基本问题（6学时）计算的历史；对问题进行抽象的典型实例——哥尼斯堡七桥问题；“梵天塔”问题；“停机问题”；算法复杂性中的难解性问题、P类问题和NP类问题；证比求易算法；P＝NP是否成立的问题；旅行商问题与组合爆炸问题；找零问题、背包问题与贪婪算法；“GOTO语句”与程序设计中的结构问题；“哲学家共餐”问题与计算机系统中的软硬件资源的管理；“两军问题”与计算机网络；“图灵测试”；“中文屋子”；计算机中的博弈问题。3．计算学科中的3个学科形态（6学时）一个关于“学生选课”的例子；抽象形态；理论形态；设计形态；3个学科形态的内在联系；计算机语言的发展及其3个学科形态的内在联系。4．计算学科中的核心概念（5学时）算法；数据结构；程序；软件；硬件；计算机中的数据（含进位制数及其相互转换，原码、反码和补码及其转换，字符、字符串和汉字，图像数据的表示，声音数据的表示等）；CC1991报告提取的核心概念。5．计算学科中的数学方法（5学时，含1个学时的讲座）数学的基本特征；数学方法的作用；集合，函数和关系，代数系统（含群、环、格、布尔代数，布尔代数与数字逻辑电路）；定义、定理和证明，必要条件和充分条件；证明方法；递归和迭代；公理化方法；形式化方法。6．计算学科中的系统科学方法（3学时）系统科学的基本思想；软件开发中为什么要引入系统科学方法；结构化方法；面向对象方法。7．社会和职业的问题（3学时）计算的社会背景；道德分析的方法；职业和道德责任；基于计算机系统的风险和责任；团队工作；知识产权；隐私和公民自由；计算机犯罪。8.探讨与展望(2学时)学科中的若干问题进行探讨，计算教育的发展与展望等内容。四、实验教学内容与要求1.存储程序式虚拟机（4学时）掌握机器指令的格式，理解机器指令系统的组成；理解“程序与数据”的同等看待；理解算法与机器的关系，了解程序在机器上的执行过程。2.结构化程序设计（3学时）熟悉顺序、选择、循环3种程序结构；掌握C语言编写选择、循环语句的方法。3.递归与迭代（3学时）加深理解递归及迭代的概念；掌握用C语言编写递归及迭代程序的方法；了解递归和迭代之间的差别。4.算法综合练习（4学时）熟悉结构化程序设计在算法中的应用；理解二分查找法的思想。5.实验考试（2学时）五、教学方法的原则建议建议由各学校学科带头人或骨干教师担任本课程的主讲，并使用投影仪进行教学，在教学过程中可穿插介绍一些计算机界著名学者的生平事迹以及我国计算机的发展历史六、考核方式及成绩构成成绩评定：平时成绩占10%，理论考试（开卷）成绩占70%，实验考试成绩占20%。七、教材与参考书目推荐教材：董荣胜.计算机科学导论——思想与方法.高等教育出版社.2007参考书目：1.董荣胜，古天龙.计算机科学与技术方法论.人民邮电出版社.2002 Brookshear著，刘艺等译.计算机科学概论（第9版）.人民邮电出版社.2007 3.许卓群，李文新，罗英伟.计算概论.清华大学出版社.2005 4.赵致琢.计算科学导论（第三版）.科学出版社.2004 5.王玉龙.计算机导论（第二版）.电子工业出版社.2004 6.黄国兴，陶树平，丁岳伟.计算机导论（第二版）.清华大学出版社.2008八、说明本大纲根据美国计算机协会（ACM）教育委员会对“整个计算学科综述性导引课程”课程的要求，以及教育部高等学校计算机科学与技术教学指导委员会编制的高等学校计算机科学与技术专业规范和IEEE/ACM制定的CC2001－CC2005有关教程编写。主讲教师李凤英讲师 李凤英（讲师） 生于辽宁、朝阳，分别于、在桂林电子工业学院获工学学士、硕士学位。至今一直在桂林电子科技大学计算机与控制学院任教，现在西安电子科技大学攻读博士学位。主要研究领域为：符号模型检验、Petri网、符号调度技术等的研究。近年来参加了国家自然科学基金、中澳国际合作等项目。

计算机专业论文参考文献

参考文献在各个学科、各种类型出版物都有着明确的标注法。以下是我为您整理的计算机专业论文参考文献，希望能提供帮助。

篇一：参考文献

[1] 刘韬，楼兴华.SQL Server2000 数据库系统开发实例导航. 北京:人民邮电出版社，2004.

[2] 丁宝康，董健全. 数据库实验教程. 北京：清华大学出版社， 2003：125-170.

[3] 孙强. 基于 的专题网站的研究与设计. 东北师范大学，2006.

[4] Michele Leroux your Apps and WCF services with Windows CardSpace. MSDN Magazine，April 2007.

[5] 肖建编. 编程实例与技巧集粹. 北京：北京希望电子出版社，2003.

[6] 巴兹拉等. 安全性高级编程. 北京：清华大学出版社，2003.

[7] Jesse C#中文版. 电子工业出版社，2006.

[8] 米切尔的等编著. 权威指南. 北京：中国电力出版社，2003.

[9] 曾登高编著..NET 系统架构与开发. 北京：电子工业出版社，2003.

[10] Jeffrey Richter. Applied Microsoft .NET Framework programming.北京：清华大学出版社， 2003.

[11] 张海藩. 软件工程导论. 北京：清华大学出版社， 2003.

篇二：参考文献

[1] 冯燕奎， 赵德奎. JSP实用案例教程[M] 清华大学出版社， 2004， 5: 70-100

[2] 王家华 软件工程[M] 东北大学出版社2001年3月303页

[3] 王宜贵 软件工程[M] 北京：机械工业出版社，2002：20-79

[4] 孙卫琴 精通struts[M]电子工业出版社 2004年8月 50-70

[5] 孙卫琴 精通hibernate[M]电子工业出版社 2005年4月 100-120

[6] 张洪斌 java2高级程序设计[M]中科多媒体出版社 2001年11月 85-90

[7] Jim Arlow and the Unified Process[M]机械工业出版社 2006年6月 30-40

[8] 林信良 技术手册[M]电子工业出版社 2006年6月 50-100

[9] 熊节、林仪明、峰、陈玉泉等主编[《CSDN社区电子杂志——Java杂志》创刊号]

[10]《程序员》杂志 2007 年第4期

[11] 耿祥义编著.JSP基础编程[M].清华大学出版社，

[12]徐建波，周新莲.Web设计原理于编程技术[M].中南大学出版社，

[13] 孙鑫编著.Java Web开发详解[M].电子工业出版社，

[14] 林上杰，林康司编著.技术手册[M].电子工业出版社，

[15] 萨师煊，王珊.数据库系统概论(第三版)[M].北京：高等教育出版社，1998.

[16] 蔡剑，景楠.Java Web应用开发：J2EE和Tomcat[M].北京：清华大学出版社，2004.

篇三：参考文献

[1]Booch G. Object-Oriented design[J]. ACM SIGAda Ada Letters. 1982，1(3)： 64-76.

[2]建模的价值IBMRational技术白皮书[R].

[3]邵维忠.杨芙清.面向对象的系统分析[M].北京：清华大学出版社.2000

[4]郑红军.张乃孝.软件开发中的形式化方法[J].计算机科学.1997，24(6)： 90-96.

[5]王一川，石纯一.基于n演算的一种Agent组织模型[J].计算机研宄与发展.2003， 40(2)： 163-168.

[6]阿丽亚娜5型火箭发射失败的调查报告[R].

[7]Booch G. Object-Oriented design[J]. ACM SIGAda Ada Letters. 1982，1(3)： 64-76.

[8]陈鑫，李宣东.基于设计演算的形式化用例分析建模框架[J].软件学报.2008，19(10)： 2539-2549

[9]夏志翔，徐中伟，陈祖希等.UML模型形式化B方法转换的实现[J].计算机应用与软件.2011，28(11)： 15-20.

[10]袁晓东，郑国梁的面向对象扩充COOZ的设计[J].软件学报.1997，8(9)：694-700.

[11]周翔.邵志清.顺序图与状态图的递归语义一致性研宄[J].计算机科学.2010，37(8)：172-174.

[12]周翔，邵志清，薛炳蔚.基于ASM的活动图一致性规则研究[J].计算机工程与设计.2009，30(19)： 4536-4539

[13]王红英.基于Petri网的软件模型验证[D].华东师范大学，2007.

[14]黄正宝，张广泉.顺序图的XYZ/E时序逻辑语义研究[J].计算机科学.2006，33(8)： 249-251.

[15]汪文元，沙基昌.谭东风.基于Petri网和UML活动图工作流建模比较[J].系统仿真学报.2006， 18(2)： 504-510

[16]Kroll P，Kruchten P. The rational unified process made easy: a practitioner's guide to the RUP[M]. Addison-Wesley Professional. 2003.

[17]Seung Mo Cho，Hyung Ho Kim， Sung Deok Cha etc al. A semantics of sequence diagrams [J]. Information Processing Letters 84. 2002: 125-130

篇四：参考文献

[1]王仁宏，数值逼近(第2版)，高等教育出版社，2012.

[2]姚永雷.Web服务自动协商机制研究(博士论文).北京邮电大学.2007.

[3]程昱.面向自治计算的自动服务协商研究(博士论文).浙江大学.2008.

[4]程皇.高济.基于机器学习的.自动协商决策模型.软件学报.2009，20(8)：2160-2169.

[5]郭静.陈英武.1-多交互协议本体的描述.计算机工程.2008，34(12)：162-166.

[6]翟社平.魏娟丽.李增智.基于概念语义协商的服务Agent划分.电子学报.2010，38(9)：2030-2034.

[7]张林兰，电子市场中的双边同步自动协商研宄(博士论文)，华中科技大学，2010.

[8]王斌.李艳.基于多Agent系统的自动协商机制及通用协商框架.计算机工程与科学.2009，31(1)：95-98.

[10]甘早斌.朱春喜.马务等.基于遗传算法的关联议题并发谈判.软件学报.2012，23(11)：2987-2999.

[11]侯薇.董红斌.印桂生.基于Bayesian学习的适应性优化协商模型.计算机研究与发展.2014，51(4)：721-730.

[12]孙天昊.电子商务中一对多协商研宄(博士论文).重庆大学.2008.

[13]吴国全.基于模式的复合服务监管关键技术研宄(博士论文).中国科学技术大学.2009.

[14]程志文.赵俊.李田等.Web服务QoS数据多源采集方法及实现.计算机科学.2009，8(8)：180-211.

[15]于卫红.基于JADE平台的多Agent系统开发技术.国防工业出版社.2011.

[16]甘健侯，姜跃，夏幼明，本体方法及其应用，科学出版社，2011.

篇五：参考文献

[1]徐福成.基于RSSI测距的无线传感器网络定位算法研宄[D].四川：西华大学，2014

[2]娄彦翔.移动无线传感器网络中节点复制攻击的高效分布式检测机制研究[D].上海交通大学、2012.

[3]孙琳.基于车载无线自俎网络的高速公路安全信息传输机制研究[D].天津：南开大学，2012.

[4]孙赫.物联网的发展与知识产权保护[D].北京：北京交通大学，2014.

[5]孙宏伟.田新广，李学春，等.一种改进的IDS异常检测模型[J].计算机学报，2004，26(11)：1450-1455.

[6]詹杰，吴伶锡，唐志军.无线传感器网络RSSI测距方法与精度分析[J].电讯技术，2010，50(4)：83-87.

[7]国务院发展研究中心产业经济研宄部，中国汽车工程学会，大众汽车集团(中国).汽车蓝皮书.中国汽车产业发展报告(2014) [M].北京：社会科学文献出版社，2014

[8]Chlamtac I， Conti M， Liu J J N. Mobile ad-hoc networking: imperatives and challenges[J]. Ad-hoc Networks，2003， 1(1)： 13-64.

[9]Choi S J， Youn H Y. An efficient key pre-distribution scheme for secure distributed sensor networks[C]//Embedded and Ubiquitous Computing-EUC 2005 Workshops. Springer Berlin Heidelberg， 2005;1088-1097.[39]Naor M，Pinkas B. Efficient trace and revoke schemes[C]//Financial cryptography. Springer Berlin Heidelberg，2001:1-20.

[10]Katsaros D， Dimokas N，Tassiulas L. Social network analysis concepts in the design of wireless ad-hoc network protocoIs[J]. Network， IEEE， 2010，24(6)： 23-29.