权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

A Study on Program Verification Systems based on Analytic Semantics

基于分析语义的程序验证系统研究

基本信息

批准号：
10680332
负责人：
MIZUTANI Tetauya
金额：
$ 1.34万
依托单位：
UNIVERSITY OF TSUKUBA
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1998
资助国家：
日本
起止时间：
1998 至 2000
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10680332/
关键词：
Verification of realtime controlled systems Envelope theory SOFA Tense Arithmetic Music information processing エンヴェローブ理論定時間システムの検証 tense Arithemetic

项目摘要

A study of verification of realtime program systems are one of the most important fields for contemporary program theory. In this research project, the investigators have developed several verification formalisms for logical and procedual programs, named SOFA, the envelope theory and the tense arithmetic, based on the analytical semantics and the analytical equivalence theory. These are to analyze and verify programs that controls discretely certain continuously physical or other external system. Each formalism describes analysis of the wake-up time of the next action from an observation time. We obtain the actual rational time value when the next action will rise, so that verification can be easier and more precise.The investigators have also researched music information processing as one of the examples of the realtime and highly intelligent program systems. They have developed and experimented realtime controlled performance systems. The design of these systems is essentially difficult because of the realtimeness and the fact that the nature of physical action and reaction by human soloists has not been understood well so far. Besides, especially, the acoustic grand piano has 0.5[sec.]delay of physical sound(i.e., the action of the corresponding key)after each input of MIDI event, so that the program must forecast human's performance in the accompaniment systems involving piano, which is another factor to make the design more complex and difficult. In order to cope with these situations and to solve various problems incurred upon with modern software techniques, they have represented specifications of these systems logically and verify these correctness using these formualisms.

实时程序系统的验证研究是现代程序理论的重要领域之一。在这个研究项目中，研究者们基于分析语义学和分析等价理论，开发了几种逻辑程序和过程程序的验证形式，命名为SOFA、包络理论和时态算法。这些是分析和验证程序，控制离散某些连续的物理或其他外部系统。每一种形式主义都描述了从观察时间分析下一个动作的唤醒时间。我们得到了下一个动作上升的实际合理时间值，使验证更容易和更精确。研究者还研究了音乐信息处理作为实时和高智能程序系统的例子之一。他们开发并试验了实时控制性能系统。这些系统的设计基本上是困难的，因为真实性和人类独奏者的物理动作和反应的本质迄今为止还没有得到很好的理解。此外，特别是，声学三角钢琴有0.5[秒。]物理声音的延迟（即，在钢琴伴奏系统中，由于每个输入事件都要经过相应的键的动作），所以程序必须预测人的演奏，这也是使设计更加复杂和困难的一个因素。为了科普这些情况，并解决与现代软件技术所引起的各种问题，他们表示这些系统的规范逻辑和验证这些正确性使用这些formualisms。