个人基本情况介绍：

教授，博士。1995年6月本科毕业于威尼斯886699计算机系计算机软件专业,先后担任十多门课程主讲，主讲课程有网络安全、系统安全、数据结构、离散数学、数据库、面向对象设计等，同时致力于软件开发，主持并编写过多项软件。于1999年任教研室副主任，2004-2010年任教学部部长、支部书记，参与教学管理工作。先后获得“教书育人风范奖”，“党员风采奖”，7次校级优秀等多次奖励。2006年师从李祥教授攻读博士学位，2009年博士毕业于威尼斯886699计算机软件与理论研究所计算机软件与理论专业。2011至2013年于中国人民大学信息学院博士后工作站，师从石文昌教授继续学习和做研究工作。研究方向是形式化方法和信息安全。

研究领域与方向：

计算机软件与理论、信息安全

科研课题（2010年以来主要承担的科研项目）：

主持美国Genechiu基金支助项目：基于行为时序逻辑TLA的基本性质规则的分析研究，编号：No.20070625，经费来源：美国Genechiu基金，起止年月：2007-03至2009-01。

主持贵州省省直工会财会软件：新工会帐务处理系统，编号：省直总工会合字2009001，经费来源：贵州省省直总工会，起止年月：2009-02至2009-12。

主持威尼斯886699项目：基于行为时序逻辑的多行为的性质规则与检测，编号：贵大人基合字（2009）021号，经费来源：威尼斯886699，起止年月：2009-11至2011-11。

主持贵州省科技基金项目：基于行为时序逻辑TLA与TLA 的加权并发行为的活性与安全性规则的研究J[2011] 2328经费来源：贵州省科技厅，起止年月2011-6至2014-5。

主持贵阳市科技项目：智能家居系统，编号：[2010]筑科成合同字第40号,经费来源：市科技，起止年月2010-5至2012-4。
主持中国人民大学科学研究基金项目：基于行为时序逻辑TLA的软件行为安全性的研究，编号：( 12 XNLF06)，起止年月2011-10至2013-5。
主持贵阳中医学院附属第一医院项目：脑病学数据库软件，起止年月2012-1至2013-1。

主持正安县政府项目：网格化智慧社区管理软件，起止年月2013-5至2014-5。

主持应用项目：智能家居APP，2015；主持应用项目：智能家居云平台，2015；主持应用项目：1讯APP，2015；主持应用项目：大数据精确招商云平台，2016；主持贵州出入境检验局项目：企业诚信云平台，2016；主持贵安国税项目：门户网站，2016；主持应用项目：固定资产清查系统与APP，2016

学术论著(2009年以来发表的论文、专著)：

[1] 万良，肖源. 一种安全转移系统模型的构造及其运用[J]. 计算机应用研究, 2014, 31(2): 558-562.

[2] 万良. 基于隔离逻辑的并行程序可靠性验证方法[J]. 计算机工程, 2014, 40(2): 86-91, 96.

[3] 万良, 石文昌, 冯慧. 基于分离逻辑的并行程序性质验证方法[J]. 计算机科学, 2013, 40(10): 148-154.

[4] 万良. An Access Control Mechanism Based on Active Domain[C]//Information Science and Engineering (ISISE), 2012 International Symposium on. IEEE, 2012: 469-472. (EI收录)

[5] 万良, 石文昌. Specifying and checking network protocol based on TLA[C]//Anti- Counterfeiting, Security and Identification (ASID), 2012 International Conference on. IEEE, 2012: 1-4.

[6] 万良. Liveness rules from fairness based on TLA. ICCSE 2011（EI收录号: 20114214434385）

[7] 万良, 李均涛. Liveness Property Safety Rules of Multi-action Based on TLA . International Conference on Internet Technology and Applications 2010（EI收录号 :20104713411804）

[8] 万良, 黄贻望, 李祥. Analysis and checking of Internet banking based on safety transition system. 2008 International Symposium on Distributed Computing and Applications for Business Engineering and Science, 907-911. 电子工业出版社, 2008.（ISTP收录号: 000259913500168）

[9] 万良, 李祥. Analysis and checking of controllable property transition system based on TLA [C]//Anti-counterfeiting, Security and Identification, 2008. ASID 2008. 2nd International Conference on. IEEE, 2008: 264-267.（收录号: 090211851802）

[10] 万良, 李祥. Analysis and Checking of Multi-Actor Liveness Rules from Fairness[C]//2008 4th International Conference on Wireless Communications, Networking and Mobile Computing. 2008: 1-4.（EI收录号 :090211846697）

[11] 万良, 李祥. Analysis and checking of safety transition system based on TLA , Engineering, Services and Knowledge Management Track 2008.（EI收录号 :090211846735）

[12] 万良, 李样. 基于 TLA 的 Kerberos 协议符号化与检测[J]. 威尼斯886699学报: 自然科学版, 2008, 24(6): 605-609.

发明专利及获奖情况（2009年以来）：

无

学术兼职及荣誉称号：

无

教学格言：

脚踏实地，梦展蓝天

电子邮件：

wanliangtr@163.com