-
公开(公告)号：CN103258081A
公开(公告)日：2013-08-21
申请号：CN201310129977.9
申请日：2013-04-15
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种抽象模型中虚假路径的高效检测方法，所述方法具体是，在反例路径中，每个状态是不是失败状态，只与它的前驱状态和后继状态有关。所以，判断时，采用并发执行，通过集合In和集合Out的交集来判断状态是否为失败状态。本发明在检测无穷反例路径时，采用有限前缀分析的多项式比已有的算法短。同时，采用并发技术，能更快的找出失败状态；而且，本发明能更早找到隐藏在反例路径中的失败状态，实验结果显示，系统的规模越大，本发明提出的方法执行的效果越好。
-
公开(公告)号：CN103257921A
公开(公告)日：2013-08-21
申请号：CN201310130862.1
申请日：2013-04-16
Applicant: 西安电子科技大学
IPC: G06F11/36
Abstract: 本发明公开了一种基于改进随机森林算法的软件故障预测系统及其方法，所述系统包括数据处理层、预测模型构建层和故障预测层，其故障预测过程是：首先计算用来得到训练模型的软件项目属性集合从而得到软件故障预测模型的训练数据集，对训练数据集进行平衡化处理；然后根据改进的随机森林算法构建预测模型；其次根据准确率以及查全率的性能限制来筛选模型；最后根据待测软件项目的属性集合信息及训练好的预测模型来对该软件项目进行预测并对预测结果和预测模型进行显示。本发明具有预测准确率高、性能稳定和执行效率高的优点，可评估最终的软件产品是否达到了规定的质量或者满足用户期望，且可指导开发人员制定软件测试和形式化验证资源的分配策略。
-
公开(公告)号：CN103176830A
公开(公告)日：2013-06-26
申请号：CN201310129978.3
申请日：2013-04-15
Applicant: 西安电子科技大学
IPC: G06F9/45
Abstract: 本发明公开了一种基于类图和活动图相结合生成C++代码的方法，其生成的过程是：由用例图转换为类图和活动图，以每一个用例为基础，根据用例图中的对该用例描述、前置条件、后置条件、控制流等信息，生成一个类图和一个活动图；建立类图和活动图到C++代码的映射规则,为了提高代码的实用性与有效性，需要将类图和活动图结合在一起来生成代码；以基于模板的技术为框架，模板引擎的输入信息选择基于模型技术中的类图和活动图，使用基于类图和活动图的模板代码生成技术生成代码。
-
公开(公告)号：CN103150200A
公开(公告)日：2013-06-12
申请号：CN201310120182.1
申请日：2013-04-08
Applicant: 西安电子科技大学
IPC: G06F9/45
Abstract: 一种计算机语言转换系统，其用于将C语言程序转换成MSVL语言程序，其包括，词法分析模块，其将字符序列转换为单词序列，所述字符序列包括C语言中的关键字、标识符、常数、运算符、头文件以及注释行的定义；语法分析模块，其基于yacc中所规定的C语言的相关词法规则，进而识别出C语言中特定的语句；转换处理模块，其根据C语言与MSVL语言之间的语言转换规律将C语言转换成MSVL语言。
-
公开(公告)号：CN103150199A
公开(公告)日：2013-06-12
申请号：CN201310120181.7
申请日：2013-04-08
Applicant: 西安电子科技大学
Abstract: 一种多类型MSVL语言解释系统其包括，变量类型声明模块、变量存储模块、算术表达式处理模块、赋值操作处理模块、强制类型转换命令处理模块及框架命令处理模块。在投影时序逻辑中及其程序设计语言MSVL中扩展了多种内置数据类型，增强了MSVL的描述能力，拓展了MSVL的应用领域，使MSVL可以更加灵活广泛地对多数据类型的系统进行建模和验证。本发明将变量的论域定义为取值和类型组成的二元组，将变量和常量的解释定义为二元组，使得每一个变量的类型作为变量的固有性质，提高变量引用的效率。针对于变量和常量的论域以及解释的扩展，给出相关函数和操作符的语义，使扩展类型后与类型相关的函数和运算符与现有的MSVL语句相兼容。
-
Patent Agency Ranking
公开(公告)号：CN102708155A
公开(公告)日：2012-10-03
申请号：CN201210118808.0
申请日：2012-04-20
Applicant: 西安电子科技大学
IPC: G06F17/30
Abstract: 本发明是一种基于回溯自动机语法分析的JSAX解析器和解析方法。通过对回溯自动机的动作转移规则δ重新定义，并将改进回溯自动机应用于语法分析器，简化了语法分析器的设计和实现，有效提高了XML解析器的效率。在进行语法分析时，回溯自动机以词法分析器提供的记号流为输入，当回溯自动机读入的记号为开始标记时，则将当前状态压入栈顶；读入记号为结束标记时则自动机从栈顶弹出一个状态，并作为自动机的下一状态；在遇到其他记号时则不进行栈操作。语法分析的同时，通过标准的回调函数将符合语法规范的XML文档信息返回给用户。本发明解决了XML文档解析器语法分析器构造复杂，性能不高的问题，具有易于实现、效率高的特点，可应用于对XML文档的解析。
-
公开(公告)号：CN102663190A
公开(公告)日：2012-09-12
申请号：CN201210102063.9
申请日：2012-04-09
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明是一种PPTL符号模型检测方法，属可信计算领域，本发明使用具有完全正则表达能力的规范语言PPTL描述待验证系统期望性质；使用Kripke结构M＝(S，R，L)描述系统模型，借助ROBDD对符号化系统模型M进行搜索，通过构建标记正则图检查期望性质公式是否可满足，节省后续操作时间，提高检测效率。本发明仅需基于时序操作符“○”的检测过程，降低了检测复杂度。本发明提升了模型检测可处理问题的规模，有效缓解状态空间爆炸问题，同时具有描述状态敏感、顺序和闭包性质的能力，可以应用于工业、农业、军事、科研等领域硬件系统设计缺陷的检测，软件系统控制逻辑错误的检查以及通信协议正确性的形式化验证。
-
公开(公告)号：CN102339232A
公开(公告)日：2012-02-01
申请号：CN201110273599.2
申请日：2011-09-15
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种基于时序逻辑语言MSVL的异步通信系统和方法，属于系统形式化建模与验证技术领域，主要涉及用形式化的方法对异步并发系统进行建模与验证。MSVL的异步通信系统包括：进程模块，通道模块和通信命令，用进程模块对异步并发系统中各个组件的行为进行建模，用通道模块对不同组件之间的通信媒介进行建模，进程模块执行通信命令实现不同组件之间的异步通信过程。本发明中进程模块之间的通道个数可根据系统的需要连接任意有限多个，通道容量可根据系统组件之间的通信需求定义所需大小，同时定义了两套通信命令以适应不同的异步通信过程。本发明可用于分布式系统的建模与验证。
-
公开(公告)号：CN101441679B
公开(公告)日：2011-06-01
申请号：CN200810232214.6
申请日：2008-11-10
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种基于扫描线方法的查找FPGA芯片空白区域的方法，其查找步骤为：从给定MKE向左查找，将所得到的连续空白单元数作为有效查找宽度w加入到有效查找宽度集合SVSW中；从该MKE的依次向上和向下找出连续空白单元数的递减序列添加到有效查找宽度集合当中，直到在FPGA中遇见边界或是已经被使用的单元为止；从SVSW中逐次选取没有查找过的w进行下述查找：检查给定的MKE是否被在同一扫描线中的其它MER用w进行查找过，如果是则停止，否则，以该MKE所在位置为右垂直边界，分别向上和向下寻找宽w的连续空白区域，并将查找所遍历的扫描线上的单元标记为以w查找过。本发明具有查找FPGA空白区域耗时少，效率高的优点，可用于基于FPGA的可重构系统中查找FPGA空白区域。
-
公开(公告)号：CN101441679A
公开(公告)日：2009-05-27
申请号：CN200810232214.6
申请日：2008-11-10
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种基于扫描线方法的查找FPGA芯片空白区域的方法，其查找步骤为：从给定MKE向左查找，将所得到的连续空白单元数作为有效查找宽度w加入到有效查找宽度集合SVSW中；从该MKE的依次向上和向下找出连续空白单元数的递减序列添加到有效查找宽度集合当中，直到在FPGA中遇见边界或是已经被使用的单元为止；从SVSW中逐次选取没有查找过的w进行下述查找：检查给定的MKE是否被在同一扫描线中的其它MER用w进行查找过，如果是则停止，否则，以该MKE所在位置为右垂直边界，分别向上和向下寻找宽w的连续空白区域，并将查找所遍历的扫描线上的单元标记为以w查找过。本发明具有查找FPGA空白区域耗时少，效率高的优点，可用于基于FPGA的可重构系统中查找FPGA空白区域。
-
-
-
-
-
-
-
-
-
Search Results
132
records
(took 0.032 seconds)
