多媒体节目时序描述的组合技术

组合性是形式描述研究的基本问题,便于大型程序的设计、分析、测试和复用.为了方便用户编制大型多媒体系统的时序描述,组合模型是必须的.目前,这样的模型有基于语言的、基于图形的、基于时间区间的和面向对象的等等.但是,这些模型描述层次过低,很难支持两个多媒体节目之间的时序描述.通过引入单位流的概念和扩展两种时序关系,研究一种多媒体节目时序描述的结构化技术,使复杂的多媒体节目易于理解,以方便用户运用组合方法把一些可以复用于不同多媒体节目的节目模块进行组合设计.     

代数规范与对象行为约束

本文研究建立了代数规范和时序逻辑规范的不同语义模型之间的关联,在结构偏代数上解释时序模态词,从而可以利用时序逻辑工具讨论由代数规范所定义的抽象对象的动态行为特征.     

基于OCPN的SMIL文档创作平台设计与实现

基于SMIL的多媒体文档创作平台是目前的应用研究重点。SMIL Authoring Tool(SAT)创作平台在参考了SMIL2．O定义基础上，以OCPN为多媒体同步时序定义的基本模型，分析了国内外现有的系统优缺点之后，利用面向对象的方法实现。SAT相对于已有的系统而言，它使用树形组织结构和OCPN对节点之间的时序和节点内部的详细同步信息进行设置，二者互相补充，可使用户进行简单的同步时序设置。     

一个统一的程序验证框架

本文提出了一个简单的方法，其中程序和其性质都由一个逻辑：时序逻辑中的公式表示．文中给出了一个程序的转换模块的定义，提出了时序执行语义的概念．它是一个时序公式，精确地说明了一个程序．将时序逻辑作为规范语言，程序正确性就意味着说明程序的公式蕴含说明性质的公式，其中蕴含即为一般的逻辑蕴含．因此，本文的方法为并发程序的规范及验证提供了一个统一的框架．它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统．一个缓冲系统的简单例子用来说明本文的方法．此例子表明本文的方法是可行的.     

基于序列图模型的多标签序列标注

该文针对实际中存在对同一句话标注多种序列标签问题,定义了多标签序列标注任务,并提出了一种新的序列图模型。序列图模型主要为了建模两种依赖关系: 不同单词在时序维度上面的关系和同一单词在不同任务之间的依赖关系。该文采用LSTM或根据Transformer修改设计的模型处理时序维度上的信息传递。同一单词在不同任务之间使用注意力机制处理不同任务之间的依赖关系,以获得每个单词更好的隐状态表示,并作为下次递归处理的输入。实验表明,该模型不仅能够在Ontonotes 5.0数据集上取得更好的结果,而且可以获取不同任务标签之间可解释的依赖关系。     

三支面向属性概念格的规则提取

在面向属性概念格和三支面向属性概念格中定义了两种协调性,并研究了两种协调性之间的关系;在三支面向属性概念格中定义了三支面向属性规则及其相应的冗余规则,并给出三支面向属性非冗余规则的刻画和算法;在决策形式背景的补背景下,进一步研究了面向属性规则和三支面向属性规则之间的区别与内在联系。     

一个多媒体数据同步模型的建立和实现

文章对多媒体数据流间存在的时序问题和时序关系进行介绍，对现有研究情况进行分析.结合一个多媒体数据模型，基于PETRI网，提出了一个同步模型，以表达媒体数据之间存在的同步关系.根据这两个模型对多媒体数据建立了相应的数据结构，并采用该数据结构介绍了对多媒体数据存取播放的实现算法.     

带有时钟变量的线性时序逻辑与实时系统验证

为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.     

基于XYZ/RE的多媒体同步器自动构造方法

XYZ系统是一个以增强软件可靠性和提高软件生产率为目的的程序开发支撑系统.它由时序逻 辑语言(temporal logic language,简称TLL)XYZ/E和以该语言为基础的一组软件工程工具组 成.为了研究XYZ系统在多媒体领域中的应用问题,介绍了一种依据多媒体对象时序描述 自动生成用XYZ/RE表示的播放同步器的方法,XYZ/RE是时序逻辑语言族XYZ/E中表示实时系统 的子语言.与相关工作比较,该方法不仅可以处理简单的时序关系,而且可以处理嵌套的时序 关系,所产生的同步器可以复用于不同的节目.     

FPGA自重构技术在雷达高度计中的应用

新一代高精度雷达高度计具有低分辨率工作模式和SAR工作模式两种方式,这两种方式的硬件工作时序是不同的,FPFA的动态可重构技术为实现这两种工作时序的切换提供了有效的手段.本文采用FPGA动态重构技术,进行了高精度雷达高度计工作时序的设计和实验验证,结果表明采用本文的方法可以正确实现高精度高度计两种硬件工作时序的切换.     

O-表达式的性质定义与规范（英文）

在所提出的程序设计方法中,赋值是物理对象上的操作,而程序则是这种操作的表达式。给出了此类表达式（O-表达式）的安全性和进展性性质的形式化定义,用实例说明了基于这些性质的形式化程序规范的模式。具有明确运行目标的O-表达式称为独立O-表达式（stand-alone O-expression,saloe）。一个完整的程序可能由若干个saloe组成。给出了一个定理,指出如何从这些saloe的性质导出完整性程序的性质。用大量实例阐明了程序性质的形式定义。     

Failure diagnosis of discrete-event systems with linear-time temporal logic specifications

The paper studies failure diagnosis of discrete-event systems (DESs) with linear-time temporal logic (LTL) specifications. The LTL formulas are used for specifying failures in the system. The LTL-based specifications make the specification specifying process easier and more user-friendly than the formal language/automata-based specifications; and they can capture the failures representing the violation of both liveness and safety properties, whereas the prior formal language/automaton-based specifications can capture the failures representing the violation of only the safety properties (such as the occurrence of a faulty event or the arrival at a failed state). Prediagnosability and diagnosability of DESs in the temporal logic setting are defined. The problem of testing prediagnosability and diagnosability is reduced to the problem of model checking. An algorithm for the test of prediagnosability and diagnosability, and the synthesis of a diagnoser is obtained. The complexity of the algorithm is exponential in the length of each specification LTL formula, and polynomial in the number of system states and the number of specifications. The requirement of nonexistence of unobservable cycles in the system, which is needed for the diagnosis algorithms in prior methods to work, is relaxed. Finally, a simple example is given for illustration.     

Tools for producing formal specifications: a view of current architectures and future directions

During the last decade, one important contribution towards requirements engineering has been the advent of formal specification languages. They offer a well‐defined notation that can improve consistency and avoid ambiguity in specifications. However, the process of obtaining formal specifications that are consistent with the requirements is itself a difficult activity. Hence, various researchers are developing systems that aid the transition from informal to formal specifications. The kind of problems tackled and the contributions made by these proposed systems are very diverse. This paper brings these studies together to provide a vision for future architectures that aim to aid the transition from informal to formal specifications. The new architecture, which is based on the strengths of existing studies, tackles a number of key issues in requirements engineering such as identifying ambiguities, incompleteness, and reusability. The paper concludes with a discussion of the research problems that need to be addressed in order to realise the proposed architecture.     

Dynamic Meta Modeling with Time: Specifying the Semantics of Multimedia Sequence Diagrams

UML offers different diagram types to model behavior and dynamics of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain. We have proposed Dynamic Meta Modeling (DMM) as a means for the specification of the formal operational semantics of UML models by applying graph transformation to the meta modeling of dynamic behavior. Within this paper, we extend this approach to also account for time by building on timed graph transformations. We apply these concepts to the domain of multimedia application modeling in which we adopt UML sequence diagrams. The DMM rules with time then specify an interpreter that can be used to analyze or test a model of multimedia sequence diagrams.     

Checking consistency in multimedia synchronization constraints

Constraint-based design is often used to correctly author a multimedia scenario due to its flexibility and efficiency. However, such a system must provide a mechanism with which users can easily manipulate the underlying structures to meet the application requirements. This paper proposes a novel method for analyzing multimedia synchronization constraints based on the constraint graph and classification, which is essential in developing efficient system support tools for constraint-based authoring systems. We specify temporal and spatial relations between multimedia objects, and use a directed graph to represent the constraints among the objects in a multimedia scenario. Moreover, we develop a method for analyzing temporal and spatial synchronization constraints based on graph theory, solving the problems of completeness checking, consistency checking, constraints relaxation and automatic spatio-temporal layout generation in a unified theoretical framework. We also discuss the effects of user interactive authoring. Compared with other methods, the proposed approach is simpler, more efficient, and easier to implement.