摘要：为提供更优质的使用Event-B形式化方法建模混合系统的工具,根据混合系统的时序约束建模方法,其能够很好刻画混合系统建模中的时间相关性质并且支持精化和组合,提出基于它的自动筛选、精化和组合的方法。开发对应的自动精化和组合的工具链,工具链包含模型检测、自动精化和组合、模型证明等一系列功能并拥有用户友好的界面。给出一个使用工具的案例介绍和应用此工具。

摘要：该研究创制一种具备自动排气功能(Auto-Exhaust function,AE)的毛管末端自动冲洗阀,以提高冲洗时长和冲洗水量。选取延时流道齿长和齿宽、上腔体容积和冲洗阀进口压力共4个因素,采用L_(18)(3^(7))正交试验设计18种规格的AE冲洗阀,并设置4种无排气装置(Non-Exhaust function,NE)的冲洗阀为对照,探究排气装置提升冲洗阀水力性能的作用机理和AE冲洗阀性能参数对试验因素的响应规律。结果表明,当进口压力为0.06~0.14 MPa时,AE冲洗阀的冲洗时长、冲洗水量和冲洗流速分别为18.2~67.7 s、3904~12367 mL和0.88~1.40 m/s。冲洗时长和水量与流道齿长、齿宽和上腔体容积均为正相关关系,与进口压力为负相关关系,冲洗流速只与进口压力有关,为正相关关系。流道齿长、齿宽和上腔体容积对冲洗时长和水量影响显著,进口压力对冲洗时长和流速影响显著(P<0.05)。AE冲洗阀能自动排出上腔体中的空气,增加蓄水容积,使其冲洗时长和水量分别比NE冲洗阀提高83.5%与75.4%以上。综合考虑延时流道抗堵塞性能、冲洗时长和水量等因素,推荐AE冲洗阀流道齿长、齿宽、上腔体容积和进口压力分别为1.2 mm、2.2 mm、19.1 mL和0.06 MPa,其冲洗时长和水量分别是NE冲洗阀的2.8和2.7倍,是进口冲洗阀的7.4和7.0倍,为67.7 s、12194 mL。研究结果可为具有排气功能的毛管末端自动冲洗阀的研发提供依据。