• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 人工智能与数据挖掘 • 上一篇    

基于CTL模型检测的胃腺癌核心路径形式化验证

王亚鹏,雷丽晖   

  1. (陕西师范大学计算机科学学院,陕西 西安 710119)
  • 收稿日期:2018-06-05 修回日期:2018-08-15 出版日期:2018-12-25 发布日期:2018-12-25
  • 基金资助:

    国家自然科学基金(F020504,A011404);中央高校基本科研业务费专项资金(GK201603086)

Formal verification of gastric adenocarcinoma
core pathway based on CTL model checking

WANG Yapeng,LEI Lihui   

  1. (School of Computer Science,Shaanxi Normal University,Xi’an 710119,China)
  • Received:2018-06-05 Revised:2018-08-15 Online:2018-12-25 Published:2018-12-25

摘要:

胃腺癌是消化系统最常见的恶性肿瘤,死亡率居消化道各类癌症之首。其发生发展是多步骤、多因素参与的复杂过程,涉及到多种蛋白分子的改变以及信号通路的异常,但其确切发病机制目前尚不清楚,研究其发病机理,探索有效治疗方法一直是医学研究最重要的课题之一。因此,对胃腺癌信号转导网络的研究有助于阐明其发病机制。目前,在胃腺癌的发生发展过程中由于基因的改变而导致细胞功能的变化,以及癌细胞环境因子通过作用于其受体和信号转导通路而影响其他正常细胞的功能。胃腺癌的信号转导网络非常复杂,通过对胃腺癌信号转导网络离散值模型的分析和验证,说明靶向胃腺癌信号通路或蛋白治疗的优越性。应用符号模型检测技术自动分析靶向信号通路或蛋白是如何影响胃腺癌细胞命运,了解胃腺癌的发生发展机理,从中找到潜在靶点,为治疗胃腺癌提供建议,使研制新的抗癌药物成为可能。
 

关键词: 模型检测, NuSMV, 细胞信号通路, 胃腺癌

Abstract:

Gastric adenocarcinoma is the most common malignancy in the digestive system, and its mortality ranks first among all types of cancers in the digestive tract. Its occurrence and development is a complex multi-step and multi-factor process which involves various protein molecules' change and abnormal signal pathways. However, its exact pathogenesis is still not clear. Studying its pathogenesis and exploring effective treatment methods have always been one of the most important topics in medical research. The study of gastric adenocarcinoma signal transduction networks therefore helps to elucidate its pathogenesis. At present, in the process of the development of gastric adenocarcinoma, there are some genetic changes that lead to changes in cell functions, and cancer cell environmental factors affect the function of cancer cells by acting on its receptors and signal transduction pathways. The signal transduction network of gastric adenocarcinoma is very complicated. We analyze and validate the discrete model of gastric adenocarcinoma signal transduction network to illustrate the superiority of targeting signaling pathways or protein therapeutics in gastric adenocarcinoma signal transduction networks. We use model detection technique to automatically analyze how targeting signaling pathways  and key proteins affect the fate of gastric adenocarcinoma cells, helping understand the mechanism of occurrence and development of gastric adenocarcinoma, find potential targets for the treatment of gastric adenocarcinoma and provide advice on the development of new anti-cancer drugs.
 

Key words: model checking, NuSMV, cell signaling pathway, gastric adenocarcinoma