This paper addresses the problem of optimal operation in long-term crude oil scheduling,which involves unloading crude oil from vessels,transferring it to charging tanks and feeding it to the distillation units.The ap...This paper addresses the problem of optimal operation in long-term crude oil scheduling,which involves unloading crude oil from vessels,transferring it to charging tanks and feeding it to the distillation units.The application of a new approach for modeling and optimization of long-term crude oil scheduling is presented and the event-tree based modeling method that is very different from mathematical programming is employed.This approach is developed on the basis of natural language modeling and continuous time representation.Event triggered rules,decomposition strategy,depth-first search algorithm and pruning strategy are adopted to improve the efficiency of searching the optimum solution.This approach is successfully applied to an industrial-size problem over a horizon of 4 weeks,involving 7 vessels,6 storage tanks,6 charging tanks,2 crude oil distillation units,and 6 crude oil types.The CPU (AMD 3000+,2.0GHz) solving time is less than 70 seconds.展开更多
A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and ...A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.展开更多
文摘This paper addresses the problem of optimal operation in long-term crude oil scheduling,which involves unloading crude oil from vessels,transferring it to charging tanks and feeding it to the distillation units.The application of a new approach for modeling and optimization of long-term crude oil scheduling is presented and the event-tree based modeling method that is very different from mathematical programming is employed.This approach is developed on the basis of natural language modeling and continuous time representation.Event triggered rules,decomposition strategy,depth-first search algorithm and pruning strategy are adopted to improve the efficiency of searching the optimum solution.This approach is successfully applied to an industrial-size problem over a horizon of 4 weeks,involving 7 vessels,6 storage tanks,6 charging tanks,2 crude oil distillation units,and 6 crude oil types.The CPU (AMD 3000+,2.0GHz) solving time is less than 70 seconds.
基金supported by the National Natural Science Foundation of China(11832012)
文摘A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.
