赵翔鹏的Blog Xiangpeng's Thinkpad

Bill Gates与Joel Spolsky对形式化方法的评价

Billg对formal methods的评价是我第一次看到。跟Joel Spolsky的评价对比一下，很有趣。

1、Microsoft 的 SDV 经验：通过静态验证提高 Windows Vista 驱动程序的质量

Static Driver Verifier (SDV) 是一种基于规则的编译时静态分析工具，用于验证用 C 代码编写的 Windows 驱动程序。SDV 根据使用 Windows 设备驱动程序接口的精确规则集对驱动程序进行验证，然后报告这些规则的任何违规行为。

Microsoft Research (MSR) Software Productivity Tools 小组投入了多年的工作来创建一种引擎，以便自动检查基于 C 的程序是否正确使用与外部库相连的接口。此项目在 MSR 中称为 SLAM，最终的成果是一个已经集成到 SDV 的强大分析引擎。

以下引用了 Microsoft Research 小组的话，来自 MSR 网站上的“提供用于技术转移的模板”：

• 选择问题。“我们选择了一个重要但并非不能克服的问题领域进行研究（设备驱动程序）。……我们有机会了解 Windows 源代码和设备驱动程序源代码。此外，我们还能够广泛接触设备驱动程序和 Windows 领域的一流专家”。

• 站在巨人的肩膀上。“SLAM 拥有几十年使用正式方法和编程语言进行研究的经验。我们非常庆幸，在 Microsoft Research、Windows Division 以及 Microsoft 之外有许多人为 SLAM 和 SDV 出策出力”。

• 研究环境。“Microsoft 的产业研究环境以及普遍的动手/实干氛围使我们能够放手尝试使用危险的解决方案来解决重大问题，还可以提供我们迫切需要的支持。”

• 软件工程。“我们采用‘开放式’的体系结构风格来开发 SLAM，对每个核心组件使用非常简单的概念接口。这使我们能够迅速使用各种工具进行试验，设定一套我们认为最能解决问题的算法。这种体系结构使我们很容易对各种组件进行重新配置以对新问题做出反应。”

• 在工作中使用正确的工具。“我们使用法国研究机构 INRIA 的 Objective Caml 函数编程语言开发 SLAM。该语言的表达力及其实现的稳定性极大地提高了生产效率。”

SDV 目前在 Microsoft 内部使用，在 WDK 的测试版本中也提供了这种工具。它的宗旨在于使 Microsoft 及其合作伙伴能够提供高质量的设备驱动程序。

比尔盖茨在 OOPSLA 2002 上的发言：

为了进行丰富的静态分析，我们已经开发了许多东西。实际上，我们花了 3000 多万美元请其他公司开发此类工具，现在我想说的是，希望您们将精力集中在将这些工具应用于大规模软件系统上，在 Windows 或 Office 的源代码中都包含此种系统，看看到我们到底能取得什么样的进展。

让我们回顾一下，就证实程序是否以特定方式运行的能力来说，有哪些尖端技术？几十年来，这种问题一直存在。当我从哈佛退学时，这曾是一个让我感兴趣并努力解决的问题，实际上当时我还在想，如果我去开一家公司，情况可能会十分糟糕，我会错过在软件程序检验方面的一些重大突破，因为我需要忙于处理员工的工资单。事实证明，看来我还并未错过太多（笑着说道），我想说的是，在某种程度上，这已经是一个非常紧迫的问题。虽然不可能实现一种完全通用的解决方案，但是对于许多非常有趣的特性，这种检验的思想已经成为可以帮助我们的长效方法，仅在去年这一点已经得到充分的体现。

我们称执行这种检验的系统为模型检查系统。您需要定义约束，包括很简单的事情：已经获取锁的人不得再次获取；没有获取锁的人不得释放锁；以及您想要确定其运行良好的代码多线程方面的内容。在本例中，您使用 C 代码本身去描述这些，然后分析程序会仔细检查并缩减程序，去掉不影响其路径分析的任何内容，进行路径分析来确定整个程序中是否有路径违反约束。

我们首次应用此解决方案的领域是设备驱动程序。

第 17 届年度 ACM 讨论会 - 面向对象的编程、系统、语言和应用程序

2、《软件随想录》：Joel Spolsky对计算机学生的七大建议

我依然清楚记得我发誓绝不读研究生的那一刻。那是在一门叫做“动态逻辑”的课程上，教师是活力十足的耶鲁大学教授Lenore Zuck，她是计算机系那些聪明的老师中最聪明的人之一。

如今， 由于记忆力糟糕， 我已经差不多把这门课的内容忘光了，但是不管怎么说，在这里我还是想要对付着说一下。大致上，形式逻辑的意思是说，如果条件成立，你就能证明结论也成立。比如，根据形式逻辑，已知“只要成绩好，就能被雇用”，然后假定“Johnny的成绩好”，你就可以得到一个崭新的结论“Johnny会被雇用”。这完全是经典方法。但是，一个解构主义者（deconstructionist）只需要10秒钟就能破坏形式逻辑中所有有用的东西。这样一来，留给你的只是一些趣味性，而不是实用性。

现在再来说动态逻辑。它与形式逻辑其实是一回事，但是必须再多考虑时间因素。比如，“你打开灯之后，就能看见自己的鞋子”，已知“灯以前是亮的”，那么这就意味着“你看见了自己的鞋子”。

对于像Zuck教授那样聪明的理论家，动态逻辑充满了吸引力，因为它看上去很有希望让你在形式上证明一些计算机程序的相关理论问题。这样做说不定很有用。比如，你可以用它在形式上证明，火星漫游车的闪存卡不会发生溢出（overflow）问题，不会因而整天一遍又一遍地重启，耽误了它在那颗赤红色的星球上漫游寻找火星人马文（Marvin the Martian）。

在第一堂课上，Zuck博士写满了整整两面黑板，甚至黑板旁边的墙上都写上了很多证明步骤。需要证明的问题是，有一个控制灯泡的开关，现在灯泡没有亮，这时你打开了开关，请证明灯泡将会点亮。

整个证明过程复杂得不可思议，处处都是陷阱，必须十分小心。保证这个证明不出错太困难了，还不如直接相信打开开关灯就会亮。真的，虽然证明过程写满了许多块黑板，但是还是有许多中间步骤被省略了，因为如果要从形式逻辑上完整证明所有步骤，那就琐碎得无法形容了。许多步骤是用各种经典的逻辑证明方法推导得到的，包括归纳法、反证法等，甚至有些部分还是由旁听的研究生证明的。

留给我们的课后作业是证明逆命题：如果灯原来是关着的，现在却亮了，那么请证明开关的状态一定同原来相反。

我动手开始证明，我真的去证明了。

我在图书馆里待了很长时间。

我对照着Zuck博士的原始证明想依样画葫芦。研究了几个小时之后，我在其中发现了一个错误。可能我抄写的时候抄错了，但是这使得我想通了一件事。如果花费3个小时，写满了一块又一块的黑板，每一秒钟都可能出错，最后能够证明的却只是一个很琐碎的结论，那么这种方式有多大的实用性呢？在活生生、充满趣味的现实世界中，你永远都不会有机会使用它。

但是，动态逻辑的理论家们对这一点不感兴趣。他们看上它不是因为它有用，而是因为它可以为他们带来终身教职。

我放弃了这门课，并且发誓绝不会去读计算机科学的研究生。

这个故事告诉我们，计算机科学与软件开发不是一回事。如果你真的非常幸运，你的学校可能会开设很像样的软件开发课程。但是另一种可能是，你的学校根本不教你在现实中如何编程，因为精英学校都觉得，教授工作技能最好留给职业技术学校、犯人重返社会的培训项目去做。你到处都能学怎么写代码。别忘了，我们是耶鲁大学，我们的使命是培养未来的世界领袖。你交了16万美元的学费，却在学循环语句的写法，这怎么可以？你以为这是什么地方，难道是机场沿途的酒店里临时拼凑起来不靠谱的Java语言培训班？哼哼。

麻烦在于我们没有一种真正教授软件开发的专门学校。你如果想成为一个程序员，你可能只能选择计算机科学专业。这是一个不错的专业，但是它同软件开发不是一回事。在那些400等级的课程代号中，去寻找名称中带有“Practicum”这个词的课程吧（编者注：指供人实习的课程）。不要被这个拉丁语单词吓倒，这些都是有用的课程，之所以起这种名字，只是为了让那些文绉绉、装腔作势、满嘴胡说八道的公司经理们觉得高深莫测。

做完了Web service，形式化方法再能做点啥？

作为一个毕业许久的人……谈起纯学术有点偏离当前本职工作的意思。不过想想这些事情还是比较有意思的。

Web service折腾了许多年，似乎已经来到了拐点。由ICWS一再延长submission date可见一斑。从理论上看，好做的都做了，没做的corner越来越少了。

再做什么呢？

云计算是一种新的商业模式，可能带来巨大利润，所以业界极为关注。但对于计算机理论研究而言恐怕没那么多新元素。虚拟化的服务器，是很好的实现技术。可它既然已经是“虚拟”的，那么形式化方法常见的abstraction思想就没有用武之地了。

当然也要想到，SOA跟RPC相比，似乎也没那么多新元素，却做出了那么多的paper……这里应该总可以找到些可以做的地方。再仔细想想。列为TODO。

无线传感器网络是个有趣的领域。与形式化方法结合，可以做一些验证的工作，比如传输协议。不过，这跟p2p可能会很像。如果早几年了解到这个领域就好了。

graphics、search、social network这些领域跟形式化方法天生就没有关系……凡是需要heruistics和statistics的地方，没法用简单的逻辑描述，就基本没有形式化方法的事儿。然而越是貌似不可能的地方，越可能隐藏着尚未发掘的矿产……虽然不好说是金矿还是铜矿。

最后，performance tuning和操作系统。一直觉得这里很有可做的东西。如果跟形式化方法的结合，可以做一些paper出来。自己太懒，没有功夫去follow学术界在这两个方向上的最新潮流，也许有些idea可以借鉴。起码这两个领域比SOA更加实在有趣。也可以考虑在这里做些工程性的东西。

其实formal methods之于计算机科学技术的其他领域，就像数学之于物理。方法和工具是现成的（比如model checking），关键是给自己定义的一大堆符号找到一个合理的解释。大牛可以直接折腾方法论本身，普通人还是老老实实的做application吧。

由无数细节组成的系统

计算机科学总是讲abstraction。这是源自数学的思维。formal methods可以说把这个发挥到了极致。但实际系统并不是这样。不要说构建Windows这样的庞然大物，就只是要写一个实用的小软件，就会遇到无数的细节。performance，security，scalability，debugging……除了functionality之外，有无数的事情要考虑。

传统的formal methods注重functionality也没错，因为在某些情形下（比如算法领域）functionality的正确性已经够难了。但这却不是软件工程中的主要问题。

我们能做的，就是尽量挣扎着把细节包装起来。比如，工程师做出一个个框架，分出若干个层次。框架可以帮助我们，但框架并不能解决一切问题，因为好的程序员必须了解各种细节。最近读一个基于ATL/WTL的真正的product code，发现这一年来看的n本书都没白看。比如，不懂C++内存布局，不懂各种calling convention，compiler的差异，就不能理解COM的设计（btw，强烈推荐《COM本质论》的第一章）。

researcher也自有办法。因为很多细节是正交的。在TASE'09上听到Zhong Shao做的invited talk，分不同的aspect去验证汇编代码的不同性质，这个是正确的思路，而且我觉得可以做更多的东西出来。以前做business process的security验证，这个也可以归到这个思路，不过high level的东西比较虚，做起来虽然不难但并不容易很深入。而Shao对汇编和机器本身建模，比如对interrupt handling建模，这个就很有新意，且竞争者较少——很多数学系出身做formal methods的人，都不太懂系统底层。

是的，跟C++和汇编相比，写Java很容易。不过事情一旦很容易，于工业上看，就不值钱了；于学术上看，就没啥好研究的了。所以，重视各种细节吧。

WinHEC 2008见闻：static code verification

WinHEC是Windows硬件开发者大会。大部分主题都是针对驱动程序开发的。作为一个技术性会议，所有的session都是微软或者赞助商的讲师在讲课，推广微软的新技术；这个跟学术性会议不同。

一个有趣的topic是static verification。微软提供的驱动开发验证器，Prefast和Static Driver Verifier，分别支持单个函数级别的验证和多函数的全局验证。简单的说它们就是两个symbolic model checker。可以验证的性质包括很多条预定义的规则，如“分配了内存就要释放，而且只能释放一次”（仅此一条规则就已经能证明这个工具的价值了），“提升了IRQL后，以后也要降低”，等等。也可以自己用类C语言写规则。

Prefast大概需要几分钟的时间来验证，SDV需要20-40分钟。（speaker说他们努力改进工具，使验证时间从20小时减少到20分钟）WDK自带这两个工具，用起来也很简单，输一条命令就会自动在后台执行验证，验证结束后会弹个提示。

为保证验证的效果，可能还要加上一些annotation：比如标明某个函数foo(char* s, int len)中，s是一个大小为len的buffer，然后就可以验证一些buffer overflow的问题。

虽然model checking的状态爆炸问题还是存在，但好在一般的驱动程序都不太复杂，所以可以说model checking已经进入工业应用阶段了，speaker说希望所有的硬件厂商们都用一下这个工具。我提了个问题，一般的C/C++程序是否可以用这两个工具来验证？回答是“you can try it”。估计小程序还是能跑一跑的。随着内存容量的不断增加，model checking是否会得到更多的应用呢？

用latex和beamer做幻灯片

做幻灯片是一件头疼的事。而用latex做幻灯片是一件很头疼、很头疼、\cdots、很头疼的事……总结和收集了一些经验如下：

• beamer教程
  
  有很多教程。对于初学者，最好先copy别人（比如师兄师姐的）模板用，或者直接看beamer的例子，C:\CTeX\texmf\doc\latex\beamer\examples。入门后，我觉得最好的提高教程是Ki-Joo Kim的Beamer v3.0 Guide，本身就是一个幻灯片，写的很清楚，看得也很爽。最后是beamer的用户手册，参考用。

• 中文幻灯片
  
  一定要定义\documentclass[cjk]{beamer}，别忘了“cjk”，否则编译不通过

• pdf书签中文乱码
  
  这是做中文幻灯片时必然遇到的问题……

  在Adobe Reader中，显示在一旁的书签(Bookmark)是Unicode的。这样一来，如果单纯是使用pdflatex生成pdf将会显示乱码。所以，若要生成中文的Bookmark就需要执行如下命令:

  pdflatex slide.tex
  pdflatex slide.tex
  gbk2uni slide.out
  pdflatex slide.tex

  注：gbk2uni是cct的一个小工具。

• 改变文字颜色
  
  \textcolor{blue!80!white}可以调色，这是xcolor包的一个功能。
  在WinEdt中要查看任何一个package的用户手册，可以在菜单中选Help-Latex doc，然后输入包名即可。

• lyx：可见即所得的Latex编辑器
  
  每个frame里几乎都要敲一遍\begin{itemize}\end{itemize；思考若干秒后决定再敲一遍（因为要缩进其中的几个\item）；再思考若干秒后把刚敲的这两行删掉（取消缩进）……用beamer就是这么痛苦。想想powerpoint，只要按Tab和Shift+Tab……于是我装了Lyx。虽然它其实还是很难用。下面是Lyx的几个经验：
  • 导入中文latex源文件前，应在latex源文件中写\usepackage[gbk]{inputenc}指定编码，否则导入后是乱码
  • Document-preferences-language改为中文，否则查看源码时有很多解码错误
  • 总的来说，还是不建议用Lyx，没有想像中得那么好。

• WinEdt宏
  
  为了从上面描述的重复劳动中解脱出来，我花了点时间看了看WinEdt的宏语言手册，写了几个简单的宏，发现还是挺好用的。
  • 为当前选中的文本增加一层itemize环境：

    BeginGroup;
    GetSel(0,1);
    CMD("Delete");
    Ins("\begin{itemize}");
    NewLine;
    Ins("%!1");
    NewLine;
    Ins("\end{itemize}");
    NewLine;
    EndGroup;

    原理很简单，把当前选中文本保存到变量%!1中，删除当前文本，然后插入适当的文本。

  • 删除当前选中文本最外层的itemize环境：

    DelLabel("","\begin{itemize}","\end{itemize}");
    就这一行。注意，一定要保证当前选中的文本中的头尾刚好是一对\begin{itemize}和\end{itemize}。

  • 自动插入任意的环境

    GetString("Input environment name:","Surround By"); // input string is saved in %!?
    BeginGroup;
    GetSel(0,1); // save current selection in %!1
    CMD("Delete");
    Ins("\begin{%!?}");
    NewLine;
    Ins("%!1");
    NewLine;
    Ins("\end{%!?}");
    IfStr('%!1','','=', "CMD('Line Up')", 'Relax'); // move one line up if current selection is empty (i.e. inserting a new environment)
    EndGroup;

    这个宏首先会提示你输入环境名，然后自动在当前选中的文本前后插入\begin{xxx}和\end{xxx}。

  • 安装宏的方法

    Help-Macro Manual，第一页就讲了这个，配了图，可能比我说的更清楚。不过这里还是大致说一下：首先把上面几个宏分别保存为.edt类型的文件，复制到WinEdt文件夹下面，例如C:\CTeX\WinEdt\Macros。然后在Options-Menu setup-Popup menus里面，选择左边的“Edit”一项，然后按上面的第二个按钮，出现新的对话框，在这里可以修改右键弹出菜单的内容，再按最上面第二个按钮，选Macro，这样就添加了一个菜单项，给它起个名字”Insert Environment“，然后在Macro编辑框中输入[Exe('%b\Macros\Insert Environment.edt');]，确定后即可在右键弹出菜单里用这个新命令了。安装其他宏的方法类似。

总结：自己动手，丰衣足食。其实早就该学一下WinEdt的这些高级功能，可以节约不少时间……

澳大利亚的PhD机会

我以前的老师、好朋友Paddy Krishnan教授在招PhD学生。对形式化方法有兴趣的同学可以联系他~Paddy人品很好，是非常nice的一个人。

Sun Microsystems Laboratories and Bond University,
Brisbane and Gold Coast, Australia
PhD Scholarship
Available to start on second semester 2008

Sun Microsystems Laboratories, Sun Labs, in collaboration
with Bond University, will sponsor a 3-year PhD scholarship in
the area of program analysis. We are interested in advanced
program analysis techniques and algorithms as they relate to
bug checking of systems code.

Requirements
Applicants must have completed a Bachelor of Computer Science, Software Engineering, Computer Engineering, Mathematics or affine area of study. The successful candidate needs good design and implementation skills in the C, C++ or Java language, as well as some knowledge of program analysis techniques in one of the following areas: data flow techniques, type analysis, or abstract interpretation. The candidate will interact with the Parfait Sun Labs team and can base his/her work on their layered framework for bug and security vulnerability checking of systems code.

See http://research.sun.com/projects/parfait for a brief description of the
project.

Supervisors

Professor Paddy Krishnan (pkrishna@bond.edu.au), Bond University, will be the PhD supervisor, and Senior Researcher and Principal Investigator, Cristina Cifuentes, Sun Labs Brisbane, will be the associate supervisor.

用Python实现一个最简单的LTL解释器

昨天在考虑一个问题：能否用LTL (Linear Temporal Logic)表示a*b*，(ab)*这两个正则表达式？前者还好写一点，但后者实在很复杂，在纸上写写画画，后来我自己都搞不清我写的公式是什么意思了。如果有个LTL表达式的解释器作测试会方便得多，但除了SPIN，手边找不到一个轻量级的工具，于是就自己写一个，选择Python是因为它支持lambda表达式，而且比较熟悉。

运行效果：
>>> F(Ischar('a'))("baac")
True
>>> U(Ischar('a'), Ischar('b'))("aaaa")
False
>>> U(Not(Ischar('b')), Ischar('b'))("aaab")
True
>>> G(Imply(Ischar('a'), F(Ischar('b'))))("aaab")
True

存在问题：
1. 只能处理有限长度的串，跟LTL的语义稍有不符，不过也足够用了。
2. 没有做Parse，所以输入必须是前缀表达式。

代码很简单：

def Ischar(ch):
return lambda s: len(s)>0 and s[0]==ch

def X(func):
return lambda s: func(s[1:])

def G(func):
return lambda s: G_impl(func, s)

def G_impl(func, s):
for i in range(len(s)):
if not func(s[i:]): return False
return True

def Not(func):
return lambda s: not func(s)

def And(f1, f2):
return lambda s: f1(s) and f2(s)

def Or(f1, f2):
return lambda s: f1(s) or f2(s)

def Imply(f1, f2):
return lambda s: (not f1(s)) or f2(s)

def F(func):
return lambda s: not G(Not(func))(s)

def U(f1, f2):
return lambda s: U_impl(f1, f2, s)

def U_impl(f1, f2, s):
i=0
while (i<len(s)):
if (f2(s[i:])): break
i += 1
if (i>=len(s)): return False
for j in range(0, i):
if (not f1(s[j:])): return False
return True
# 到此就定义了LTL的各种算子。

# 判定a* b*：
def astar_bstar(a,b):
return lambda s: G(Imply(Ischar(b), G(Not(Ischar(a)))))(s)

# 下面是为定义(ab)*所写的辅助函数，参考了DecSerFlow的定义（所以才用了奇怪的B_always_between_A，而不是定义A_always_between_B）。
def existence(a):
return lambda s: F(Ischar(a))(s)

def response(a, b):
return lambda s: G(Imply(Ischar(a), existence(b)))(s)

def precedence(a, b):
return lambda s: Imply(existence(b), U(Not(Ischar(b)), Ischar(a)))(s)

def B_always_between_A(a,b):
return lambda s: G(Imply(Ischar(a), X(precedence(b, a))))(s)

# 判定(ab)*：
def ab_star(a,b):
return lambda s:  And(precedence(a,b), And(response(a,b), And(B_always_between_A(b,a), B_always_between_A(a,b))))(s)

# 测试一下：
if __name__ == "__main__":
assert ab_star('a','b')("")==True
assert ab_star('a','b')("a")==False
assert ab_star('a','b')("b")==False
assert ab_star('a','b')("ba")==False
assert ab_star('a','b')("abab")==True
assert ab_star('a','b')("ababa")==False
assert ab_star('a','b')("ababb")==False
assert ab_star('a','b')("abaab")==False

assert astar_bstar('a','b')("aabb")==True
assert astar_bstar('a','b')("abab")==False
assert astar_bstar('a','b')("bbaa")==False

看起来我的定义似乎是对的，虽然我也无法证明这个正确性。我比较困惑的是LTL和正则表达式的关系，查了一本书说是LTL的表达能力不如正则表达式，LTL的表达能力与star-free regular expression相同？但上面的例子却说明(ab)*, a*b*是可以用LTL表达的？搞不懂。

Update: 原来是我对star-free的理解不对，参照Loop-Free Alternating Finite Automata一文的说法，所谓“star-free的regexp语言”虽然不含有*，却包含negation和intersection，因此它可以表达某些无限长的串，究竟是哪些？不是那么容易说清楚。

如果LTL可以表达(ab)*，那就说明(ab)*一定可以转换为star-free regexp的形式。尝试一下：先定义L=\neg (aa) \intersection \neg (bb)，则L表示ab交错的序列，但不保证a是第一个字母；稍微改进一下，(a L)  \intersection  L应该就是一个正确的表示吧。

什么是科学工作流(scientific workflow)

科学家们，例如天文研究者，要想协作科研的话，就需要共享大规模的数据，相当于做些分布式计算。这个数据的流动过程随着研究机构的增多可能越来越复杂，以至于需要独立出来专门管理，这就是scientific workflow的大概意思。scientific workflow貌似是一个新方向，讨论班上听别人讲了一篇，后来帮人审稿看到一篇，今天发现12月的Computer杂志上还登了一篇文章。

Computer杂志上这篇介绍scientific workflow的文章全是文字，几乎连个数字都没有，读完之后觉得有点空洞。这scientific workflow跟business workflow的区别说大也大，说小也小。列举几个scientific workflow的特色/需求：

可重复性：这是科学研究的基本要求，但其实很难做到，因为系统是分布式的，数据也是分布式的，谁也不好说哪个数据能一直存在。说不定过几年系统一升级，以前的程序就不能运行了；谁叫计算机软件的基础架构天天改呢？

著作权问题：科学家的数据都很珍贵，workflow的流程、以及每个端点运行的程序也是不能随便公开的，不然被人剽窃了怎么行。但是又要把自己的研究结果给别人看，至少要给评审的人看，不然怎么让别人赞同你的工作呢？而分布式的workflow意味着最后的成果是大家共享的，因此更要算清楚每部分工作都是谁的成果。所以，每次运行所得到的数据上要附有元信息以说明这个数据是运行了谁的workflow，都用到了谁提供的数据。最好有一种抽象机制，能自动提取出个大概，让人看了很佩服却无法复制。

著作权问题也说明scientific workflow的异构性，需要处在不同地理位置的多方共同合作。

探索性的经常修改：科学家需要不断地调整workflow的参数甚至是修改控制流程来尝试得到新结果，但他们又不像流程设计师那么专业，所以要提供一个易用的接口。

其他的特性就是一些无聊的buzzword，像“更灵活(flexibility)”、“更好的伸缩性(scaling)”、要考虑security之类的问题。

总结：虽然没有本质的新东西，但在搞CS的人眼里看来，sci workflow毕竟是计算机研究这个大bbs开的一个新版，正是灌水的好地方，大家快去抢位置吧。把workflow旧版里的帖子稍加处理一下转载过来，又是一篇新文章，说不定还有人给你m一下呢。

近期形式化方法相关学术报告/课程

ARTIST2/UNU-IIST 嵌入式系统设计2007暑期研讨班， 苏州，2007年8月1-10号。
ARTIST每年都会在国内举办一个summer school。我去听过去年在西安的课程。

Modal Logic, Invariance, and the Fine-Structure of Classical Logic
Professor Johan van Benthem from University of Amsterdam

Thursday, 2nd Aug
9:15am--11:30am Modal Logic, Invariance, and the Fine-Structure of Classical Logic 中科院软件所5号楼3层39号会议室

Friday, 3rd Aug
9:30am--11:30am Mini-Course part 2,3 中科院软件所5号楼3层39号会议室
"Modal Logic, Invariance, and the Fine-Structure of Classical Logic"