• XiaopingWang posted a new activity comment 2y,10mo

    In reply to: XiaopingWang posted an update 高阶逻辑辅助证明系统 [德] 托比亚斯·尼普科夫,[英] 劳伦斯·鲍尔森,[德] 玛尔库斯·温泽尔 著; 陈光喜,刘卓军 译 View

    我瞎议一下,不一定正确。可靠性和安全性是两个不同的概念,对于安全(Safety)关键软件系统而言,我们关注OS和应用的安全目标,如安全属性、安全完整度是否达到预定的要求。应该说没还有任何一个应用产品可以保证完全地实现理想的安全目标,最主要的原因在于计算机系统的核心——OS往往无法提供理想的安全服务和安全保障。这主要存在 2 个方面的原因:(1)在 OS 实现过程中, OS 开发者不可避免地存在编程错误、实现与设计不一致等问 题; (2)更重要的是, 在 OS 设计过程存在 OS 功能设计与安 全目标不一致等问题。形式化方法是指使用基于 数学逻辑和各种推理验证的技术来描述、开发以及验证软件和硬件系统的方法。利用形式化方法对 OS 进行设计和验证, 包括利用严格的数学形式方法描述 OS… Read more

  • XiaopingWang posted a new activity comment 2y,10mo

    In reply to: XiaopingWang posted an update 目前为止,seL4是第一个经过形式化验证并证明功能正确性的完整的通用的操作系统内核。 seL4所能达到的功能如下: […] View

    OS 形式化设计和验证技术需要在以下的方面有所突破:
    (1) 在 OS 模型设计方面, 将系统的功能需求和安全策略的非形式化描述与 OS 模型的形式化描述有机地结合,便于后期对两者一致性的验证。
    (2) 在形式化验证工具方面,验证工具采用的验证逻辑要更加 贴近程序逻辑,便于将系统实现代码转化为验证代码。
    (3) 在 OS 实现代码方面,所采用的编程语言要加入验证逻辑的概念, 使编程语言起到描述和验证的桥梁作用。
    (4) 在验证重用方面, 对系统功能模块的验证要和程序逻辑相分离, 便于将 已有的验证工作应用到后续的验证任务中。

  • XiaopingWang posted a new activity comment 2y,10mo

    In reply to: XiaopingWang posted an update 目前为止,seL4是第一个经过形式化验证并证明功能正确性的完整的通用的操作系统内核。 seL4所能达到的功能如下: […] View

    国内相关的工作来自南京大学的博士生钱振江,下面三篇文章:
    操作系统形式化设计与安全需求的一致性验证研究
    钱振江; 黄皓; 宋方敏;
    南京大学计算机科学与技术系; 常熟理工学院计算机科学与工程学院; 伦敦大学国王学院;

    【摘要】… Read more

  • XiaopingWang posted a new activity comment 2y,10mo

    In reply to: xilongpei posted an update in the group OS-Kernel General Dynamics 收购 Open Kernel Labs (OK Labs) View

    喜龙,刚刚发了两个有关OS形式证明的帖子。Sorry,一直没有时间关注这个问题。

  • XiaopingWang posted an update 2y,10mo

    高阶逻辑辅助证明系统
    [德] 托比亚斯·尼普科夫,[英] 劳伦斯·鲍尔森,[德] 玛尔库斯·温泽尔 著; 陈光喜,刘卓军 译

    • xilongpei replied 2y,10mo

      请教@xpwang “通过形式证明的方式”与“通过设计与测试的方式” 哪种方式对提高软件可靠性更要?我看了一下形式证明的东西,感觉很复杂,它对提高软件可靠性真的十分有意义吗?因为,为了支持形式化证明,操作系统本身需要通过Haskell这样的语言实现,然后再编译成c/c++,再编译成目标码。
      真心请教。怕因为我的无知而做出简单的思考,最后做出的操作系统,还是个普通的操作系统,没啥实质的创新。
      @wwang

      • 我瞎议一下,不一定正确。可靠性和安全性是两个不同的概念,对于安全(Safety)关键软件系统而言,我们关注OS和应用的安全目标,如安全属性、安全完整度是否达到预定的要求。应该说没还有任何一个应用产品可以保证完全地实现理想的安全目标,最主要的原因在于计算机系统的核心——OS往往无法提供理想的安全服务和安全保障。这主要存在 2 个方面的原因:(1)在 OS 实现过程中, OS 开发者不可避免地存在编程错误、实现与设计不一致等问 题; (2)更重要的是, 在 OS 设计过程存在 OS 功能设计与安 全目标不一致等问题。形式化方法是指使用基于 数学逻辑和各种推理验证的技术来描述、开发以及验证软件和硬件系统的方法。利用形式化方法对 OS 进行设计和验证, 包括利用严格的数学形式方法描述 OS… Read more

      • WeiWang replied 2y,10mo

        从测试的角度理解是,通过形式化证明的系统是bug free的,而传统的测试很难保证没有潜在的bug。所以形式化方法在安全有关的软件中是非常重要的,另一个已经广泛使用的领域是硬件,像Intel都在硬件设计上面使用形式化方法,以保证经过形式化验证的的硬件完全符合规范。但是现在主要的矛盾是随着硬件和软件复杂度增加,形式化验证的可行性收到挑战,比如如何对复杂形体建模,而且很多验证算法都是NP的(比如模型检测的思想其实就是穷举),实践起来很难。这也是为什么现在在OS上面,只有最核心的kernel方面的验证,代码一复杂,形式化方法就非常难了;而且之所以要用到Haskell,肯定也是目前对C/C++直接验证具有一些技术上的难度。所以,简单来说,“通过形式证明的方式”比“通过设计与测试的方式”… Read more

    • WeiWang replied 2y,10mo

      谢谢王老师推荐的书~

  • XiaopingWang posted an update 2y,10mo

    目前为止,seL4是第一个经过形式化验证并证明功能正确性的完整的通用的操作系统内核。 seL4所能达到的功能如下: … Read more

    • 国内相关的工作来自南京大学的博士生钱振江,下面三篇文章:
      操作系统形式化设计与安全需求的一致性验证研究
      钱振江; 黄皓; 宋方敏;
      南京大学计算机科学与技术系; 常熟理工学院计算机科学与工程学院; 伦敦大学国王学院;

      【摘要】… Read more

      • OS 形式化设计和验证技术需要在以下的方面有所突破:
        (1) 在 OS 模型设计方面, 将系统的功能需求和安全策略的非形式化描述与 OS 模型的形式化描述有机地结合,便于后期对两者一致性的验证。
        (2) 在形式化验证工具方面,验证工具采用的验证逻辑要更加 贴近程序逻辑,便于将系统实现代码转化为验证代码。
        (3) 在 OS 实现代码方面,所采用的编程语言要加入验证逻辑的概念, 使编程语言起到描述和验证的桥梁作用。
        (4) 在验证重用方面, 对系统功能模块的验证要和程序逻辑相分离, 便于将 已有的验证工作应用到后续的验证任务中。

  • XiaopingWang posted a new activity comment 2y,11mo

    In reply to: xilongpei posted an update in the group OS-Kernel General Dynamics 收购 Open Kernel Labs (OK Labs) View

    好,我有空去看看弯曲。

  • XiaopingWang posted a new activity comment 2y,12mo

    In reply to: XiaopingWang posted an update […] View

    用于软件形式验证技术很多,如形式规约、模型检测、定理证明等等,Isabelle是一种基于高阶逻辑的辅助定理证明系统, 类似的还有很多,恐怕比较有名的还是交互式定理证明工具Coq。目前,如何有效地集成形式程序验证与领域专用语言(DSL)和逻辑(Logics)是个大问题。

  • XiaopingWang posted a new activity comment 2y,12mo

    In reply to: XiaopingWang posted an update […] View

    刚才已经邮件发送给你。

  • XiaopingWang posted a new activity comment 2y,12mo

    In reply to: XiaopingWang posted an update […] View

    操作系统对象语义模型(OSOSM)及形式化验证 http://www.cnki.com.cn/Article/CJFDTotal-JFYZ201212028.htm
    钱振江 刘苇 黄皓 《计算机研究与发展》 2012年12期 加入收藏 投稿

  • XiaopingWang posted an update 2y,12mo

    到现在为止软件工程学并没有改变软件的尴尬境地,应用软件如此,系统软件更是如此,成也操作系统,败也操作系统。软件是信息技术系统产品的灵魂,带给人们财富,同时也带给人们灾难。严格软件开发方法的探索一直在进行,不同学术研究小组纷纷提出了自己的基于不同层面的验证方法与框架,试图提升软件的可验证性与可证实性,以此来保障软件的可靠运行。强化的条件约束与低效的灵活性是一对不可调和的矛盾主题。传统架构与方法的牢固现实束缚了新方法、新模式、新框架的落地生根,尽管验证的研究思路多样化,但真正落实到工程中的更是难上加难,造成落实难是多因素的。安全攸关软件研制有时也粗制滥造,形成用起来难、不用危险的两难境地。
    从软件形成的各个环节与层面考虑,包括多方面的急需处理的难题,语言、语言处理、执行环境与操作系统的安全及可靠契合、外部环境因… Read more

  • XiaopingWang posted an update 3y

    日本电子技术综合研究所与NEC合作研究的数字型进化LSI,将PLD部、遗传算法实现部以及作为外部接口的CPU集成在一块芯片上,并应用开发了假手和自治式移动机器人。 当人的手臂肌肉运动时,皮肤表面会产生一定的电位,不同的动作如握紧、松开等,筋力的模式各有不同。用进化硬件的方法自动识别不同模式的筋力,即在进化硬件上实现这种模式识别电路,从而实现控制假手动作的目的。先前开发的控制型假手用多个系列适应不同患者的需要,通常患者需要1个月左右才能比较适应,用进化硬件方法开发的假手能够在发生伤残后立即使用,很快适应患者的肌肉萎缩变化。该产品已在1998年商品化。

  • XiaopingWang posted an update 3y

    新民网6月21日报道:身体像被冰雪“冻住”,今天是腿,明天是手,最后连控制眼球转动的肌肉也不例外……这是一种罕见病——神经肌肉疾病被世界卫生组织(WHO)确认为五大绝症之一,比癌症更残忍更难治。
    据《今日日本》6月19日报道,最近日本一家机器人制造商展示了一款智能穿戴设备,该产品可通过穿戴者的思维控制达到“增幅”肢体动作的效果,让穿戴者变成“大力士”。据悉,该设备运作过程如下:首先,穿戴者的大脑向肢体传递移动信息;然后,该设备检测出皮肤上流动的微弱电脉冲信号;接着,该设备自动配合肢体作出移动反应。在智能设备的帮助下,穿戴者能发出比平时更大的力量。据悉,该设备不仅能帮助老年人和残疾人出行,还能帮助工人们举起重物。

  • XiaopingWang posted a new activity comment 3y

    In reply to: XiaopingWang posted an update […] View

    我认为,选择合适的应用领域比较重要,因为应用有些特定的需求是比较关键的,如铁路和地铁的系统要求高安全,故障导向安全,现在的ATP、ATO、CBTC系统更是如此,要求严格的软件开发(软件形式化验证)、容错设计(如三模冗余等)。 另外,地铁或高铁的门槛很高,不如民用机器人的任务导向,入口容易。

  • XiaopingWang posted an update 3y

    Linux的致命缺陷在于它不是一个硬实时操作系统。实时操作系统(RTOS)有一系列严格的定义:包括严格按照任务优先级抢占执行,快速的中断响应,对关中断的时间有非常严格的控制,实时系统都要求重要任务先执行,不重要的任务往后放,Linux内核设计并没有考虑到这些点,Linux的主要应用还是在通用计算机和服务器方面,在工业控制、自动化方面还有各种各样的操作系统:ucos,nuclues,threadX,greenhill,VxWorks等等。

    • xilongpei replied 3y

      我现在的想法是设计一个Linux这样的分时操作系统与QNX(或L4)这样的实时操作系统的混搭的操作系统,上面通过Runtime提供统一的编程模型。操作系统的实时性要求它减少封中断(CLI)的时间,而且要求内核随时可重入,这与操作系统的业务处理能力与规模都是矛盾的。 @wwang

      • XiaopingWang replied 3y

        我认为,选择合适的应用领域比较重要,因为应用有些特定的需求是比较关键的,如铁路和地铁的系统要求高安全,故障导向安全,现在的ATP、ATO、CBTC系统更是如此,要求严格的软件开发(软件形式化验证)、容错设计(如三模冗余等)。 另外,地铁或高铁的门槛很高,不如民用机器人的任务导向,入口容易。

  • XiaopingWang posted a new activity comment 3y

    In reply to: XiaopingWang posted an update 上世纪70 年代末成立了家酿计算机俱乐部(Homebrew Computer Club), 今天则是家酿机器人俱乐部(Homebrew Robotics Club)的时代。 View

    I see. 与早期分布的总线结构不一样,与EJB的基于容器的构件技术相似,但不同的是分别运行在不同OS核上,可以轻量化、容错处理,实时性满足。

  • XiaopingWang posted a new activity comment 3y

    In reply to: XiaopingWang posted an update 上世纪70 年代末成立了家酿计算机俱乐部(Homebrew Computer Club), 今天则是家酿机器人俱乐部(Homebrew Robotics Club)的时代。 View

    是的,树莓派、Arduino 也有不少开源的工作用于机器人的. 此外,有两个平台/例子参考:
    (1)乐高的机器人操作系统,制作魔方机器人http://www.diy-robots.com/?page_id=46
    (2)基于Ubuntu的ROS,http://www.ros.org/
    Elastos除了独立知识产权外,有哪些优势?

  • XiaopingWang posted an update 3y

    上世纪70 年代末成立了家酿计算机俱乐部(Homebrew Computer Club), 今天则是家酿机器人俱乐部(Homebrew Robotics Club)的时代。

    • xilongpei replied 3y

      Elastos在象机器人这样的混合计算(机器人是由多个控制系统组合在一起的联合计算系统)场合,有机会,它的构件技术,比web耦合得紧,比RPC耦合得松。@jingyu @luozhaohui

      • XiaopingWang replied 3y

        是的,树莓派、Arduino 也有不少开源的工作用于机器人的. 此外,有两个平台/例子参考:
        (1)乐高的机器人操作系统,制作魔方机器人http://www.diy-robots.com/?page_id=46
        (2)基于Ubuntu的ROS,http://www.ros.org/
        Elastos除了独立知识产权外,有哪些优势?

        • xilongpei replied 3y

          @caojing @luozhaohui Elastos的最大优势是它的构件技术架构,可以把构件理解成封装了的类(class),构件可以分为N个群集(容器),每个群集分别运行在不同的OS核上,就是把N个核的分散式计算整合成一个计算,而这时的编程模型是一个统一的模型,计算管理也是象管理一个计算单元那样。
          因为同时跑在N个OS核上,所以能满足高可靠性(容错、冗余)、实时性的要求。

          • XiaopingWang replied 3y

            I see. 与早期分布的总线结构不一样,与EJB的基于容器的构件技术相似,但不同的是分别运行在不同OS核上,可以轻量化、容错处理,实时性满足。

  • XiaopingWang posted a new activity comment 3y

    In reply to: XiaopingWang posted an update […] View

    底层的问题应该比较简单,上层面向应用很复杂,五花八门。硅谷Willow Garage的PR2(也是UC Berkeley的一个机器人项目)比较典型。我刚才又贴了一篇博文请参考,综合了国内外的一些情况。另外,我得科网博客转载了一篇来自科学院合肥所的文章“机器人与关键技术解析”:http://blog.sciencenet.cn/blog-1225851-788677.html,今年5月的IEEE Spectrum也有不少文章可以做一般了解。

  • XiaopingWang posted an update 3y

    2010年UC Berkeley研究人员搞了一个机器人折毛巾的PR2,有两个大手臂,脸上有6个摄像头,这个对我们来说并不是很困难的动作,对机器人来说却是相当地复杂。因为,没折好的毛巾是个不规则的形状,不是那么容易辨识,而在拿起来折迭的过程中,毛巾又会不断的变形,更增添机器人辨识的困难度。… Read more

  • Load More