个人基本情况介绍：

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

研究领域与方向：

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

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

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

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

主持贵州大学项目：基于行为时序逻辑的多行为的性质规则与检测，编号：贵大人基合字（2009）021号，经费来源：贵州大学，起止年月：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]. 贵州大学学报: 自然科学版, 2008, 24(6): 605-609.

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

无

学术兼职及荣誉称号：

无

教学格言：

脚踏实地，梦展蓝天

电子邮件：

wanliangtr@163.com