基于网语言的Ada程序局部性质的分析和验证

旨在研究利用网语言讨论Ada程序性质和由此而引起的Ada网的状态爆炸问题.研究了Ada网的同步合成与分解,讨论了它们的语言性质,并利用这一结果分析和验证了Ada程序的安全性和活性,从而为复杂的Ada程序的分析与验证提供了一个新的有效途经.     

从软件工程看Ada程序设计语言

Ada语言是一种新的现代高级程序设计语言,它代表了现代高级程序设计语言的发展水平。本文从软件工程的角度分析了Ada语言所具有的主要特征和这些特征对软件工程的支持及贡献。目的在于更深入地认识Ada语言及其作用,促进在软件工程领域中更好地开发应用Ada语言。     

Ada中实时结构的Petri网建模与分析

本文从一般时间网出发，派生出一种简单时间网，并建模了延迟，分支选择，异步选择，优先权等Ada实时结构，特别是把优先权处理为一种时间特性，这样不仅扩充了Petri网在Ada中的建模能力，同时可以更加准确刻画Ada程序行为。     

VAX／VMS Ada异常的实现方法

程序单元的运行可能会遇到程序无法正常运行下去的出错(或例外)情况。在Ada语言中引入了异常机制,以处理程序运行中出现的这些错误或例外情况。异常机制是Ada语言程序运行期间处理异常的方法和手段,是Ada语言的一个重要特点,也是实时程序设计所要求的重要设施。本文主要讨论Ada异常机制的语义、以及VAX/VMS Ada实现这一机制使用的数据结构和实现方法。     

P—Ada：一个基于工作站机群的Ada95编译系统

Ada95语言是一种功能十分强大的高级程序设计语言,其诸多特征,例如强类型检查,数据抽象以及面向对象等,反映了现代软件工程的要求,便于程序员开发高可靠性、高可移植性的大规模实时软件系统。在并行处理方面,Ada95语言提供了任务描述机制用以支持并发程序设计。在现有的Ada95编译器中,任务机制一般都是在单机上或共享内存的多机系统上利用多线程实现的,因而在不存在共享内存的松散耦合的系统中无法使用。     

并发程序验证的时序Petri网方法

并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。     

Ada语言回顾与展望

本文概述了 Ada 语言的研制背景与过程,讨论了 Ada 与其它语言的区别、Ada 的成就与不足,分析了 Ada 的现状并展望了 Ada 的未来。     

Ada任务死锁动态检测工具

本文介绍“Ada任务死锁动态检具工具”是根据美国斯坦福大学David C. Luckham等人的思想自行设计开发的。该工具包括两部分——预处理器(preprocessor)和死锁检测器(monitor)。本文首先简述Ada语言的任务机构,然后定义该工具所能检测的几种变锁,提出检测各种变锁的算法及实现时所用的主要数据结构和用户接口问题,介绍如何对程序进行正文交换,最后给出简要结论。     

Ada语言与Occam语言的比较

一、引言过去十年在计算语言领域的重要进展之一是出现了具有并行计算能力的Ada语言和Occam语言。Ada语言是具有类似Pascal语言的控制结构,并且能重植入过程和函数的大型语言,其初始设计目标是满足美国国防部所规定的要求,即首先考虑支持适于军事装备的嵌入式编程系统。就本质而言,Ada语言是在串行语言的结构上,扩充增加了并发执行的能力。 Occam语言是和Transputer同时设计实     

VAX／VMS Ada编译优化功能,结构和方法

Ada语言一个显著的特点是可用于实时控制,要求目标代码的质量很高,所以优化(包括时间,空间)在编译中占有举足轻重的地位。优化功能在Ada编译中是个可选项。编译时,如果加入命令项/NOOPTIMIZER,则不进行优化处理,否则,就对之进行优化处理。由此可知,优化程序在编译中是完全独立的部分。VMS支持下的Ada编译优化功     

Ada95语言评述

Ａｄａ９５语言是在Ａｄａ８３基础上修订而成的，它几乎提供了现代程序设计范型及程序设计实践所需要的一切设施，它可以支持面向对象的程序设计、大型程序设计、实时与并行程序设计等等。     

审计缓冲区的形式化模型及其验证

审计系统作为安全信息系统的一个重要组成部分,对于监督系统的正常运行、保障安全策略的正确实施、构造计算机入侵检测系统等都具有十分重要的意义。审计缓冲区的管理是审计系统的核心部分,本文利用时序Petri网对审计缓冲区管理的实现方案进行建模,进而对系统的安全性和活性进行了分析和验证。该方法利用时序逻辑扩充了Petri网缺乏描述系统事件之间时序关系的局限性,同时发挥了Petri网对系统并发和物理结构的有效描述及分析的优势,达到了系统验证的目的。     

基于规则的代码构件提取技术研究

构件提取是构件化技术中的一个热点问题,采用程序树作为代码构件的一种形式化表示,并使用结构化标记文法来解决构件提取中规则描述的问题。使得提取技术具有跨语言的能力,并给出了基于结构化标记规则的Ada代码构件提取过程实例。     

Ada并发软件的图形化设计方法研究

研究的目标：为Ada并发软件的设计提供一种图形化的方法和支撑工具,以便用图形表达并发软件的设计,并生成并发程序的框架（并发程序单元的划分和它们之间的通信）。这样做的好处在于提高软件的生产率,改善软件质量。在提出用于并发软件理解的会合次序图的基础上,给出了并发设计语言CONDL的语法、语义描述和图形化表示（泳道）,并简单介绍了所研制的一个工具CONDLAS（生成Ada代码框架）。     

Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

This paper presents some results of integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems. The intention of this research is to use predicate transition nets as a specification method and to use first order temporal logic as a verification method so that their strengths — the easy comprehension of predicate transition nets and the reasoning power of first order temporal logic can be combined. In this paper, a theoretical relationship between the computation models of these two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; and a special temporal refutation proof technique is proposed and illustrated in verifying various concurrent properties of the predicate transition net specification of the five dining philosophers problem.     

基于AdaBoost特征约减的入侵检测分类方法

提出一种基于AdaBoost的入侵特征约减算法,利用该算法约减入侵特征中的冗余特征,构造Ada-加权和Ada-域值分类器,并与支持向量机分类器进行对比。设计并实现Linux实时入侵检测实验平台,并将特征约减算法和3种分类方法应用于该平台。实验结果表明,由特征约减算法挑选出来的入侵特征集较优,Ada-加权和Ada-域值分类器的分类效果优于支持向量机分类器,且Ada-域值分类器在测试集上的检测性能最佳。     

TCPN的组合可调度分析

时间约束Petri网(Timing Constraints Petri nets,简称TCPNs)是一类重要的时间Petri网系统.针对TCPNs中变迁可调度原始语义的不足,本文对相关定义重新定义,丰富并完善了TPCNs理论.本文首先给出了新的针对单个变迁或变迁序列的可调度分析策略.如果一个特定的变迁序列是可调度的,则相应的活动序列也同样可以顺利地完成自身的执行;否则,不可调度的变迁需要调整自己的时间约束;然后提出了组合式的可调度分析策略以分析复杂变迁序列,最后提出时序一致性的概念.     

TeMAS–a multi-agent system for temporally rich domains

In this paper, we present the model and simulator of a multi-agent system (MAS) for temporally rich domains. The theoretical foundations of the model include a knowledge representation scheme based on an original modification of Petri nets, called Petri nets with time tokens (PNTTs), as well as temporal reasoning based on the extension of Allen's temporal logic. The proposed MAS, called TeMAS, has a hierarchical structure, consisting of different levels, where each level contains clusters of agents. A paradigm of hierarchically organized blackboards is used for the communication among agents, clusters, as well as levels. We describe an object-oriented implementation of a program simulator of TeMAS and give an example of the use of the simulator for interpretation of events in a dynamic scene. Slobodan Ribarić received the B.S. degree in electronics, the M.S. degree in automatics, and the Ph.D. degree in electrical engineering from the Faculty of Electrical Engineering, Ljubljana, Slovenia, in 1974, 1976, and 1982, respectively. He is currently a Full Professor at the Department of Electronics, Microelectronics, Computer and Intelligent Systems, Faculty of Electrical Engineering and Computing, University of Zagreb, Croatia. His research interests include pattern recognition, artificial intelligence, biometrics, computer architecture and robot vision. He has published more than 150 papers on these topics and authored four books (Microprocessor Architecture, The Fifth Computer Generation Architecture, Advanced Microprocessor Architectures, CISC and RISC Computer Architecture) and co-authored one book (An Introduction to Pattern Recognition). Dr. Ribarić is a Member of the IEEE, ISAI and IAPR. Tomislav Hrkać received the B.S. degree in computer science from the Faculty of Electrical Engineering and Computing at the University of Zagreb, Croatia, in 1999. Since October 2000, he has been a Researcher with the Department of Electronics, Microelectronics, Computer and Intelligent Systems at the same faculty. He received the M.S. degree in 2004. As a co-author, he published several papers in international conference proceedings and a paper in a reviewed scientific journal. He is a Student Member of IEEE.