http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/11375 Sun, 17 May 2026 22:20:45 GMT 2026-05-17T22:20:45Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12798 Title: Modeling and verification of safety critical systems: A case study on pacemaker Authors: Tuan L.A.; Zheng M.C.; Tho Q.T. Abstract: The pacemaker challenge proposed by Software Quality Research Laboratory is looking for formal methods to produce precise and reliable systems. Safety critical systems like pacemaker need to guarantee important properties (like deadlock-free, safety, etc.), which concern human lives. Formal methods have been applied in designing safety critical systems with verified desirable properties. In this paper, we propose a formal model of pacemaker, modeling its behaviors and its communication with the external environment, using a real-time formalism. Critical properties, such as deadlock freeness and heart rate limits are then verified using the model checker PAT(Process Analysis Toolkit). This work yields a verified formal model of pacemaker systems, which can serve as specification for real pacemaker implementations. © 2010 IEEE. Fri, 01 Jan 2010 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12798 2010-01-01T00:00:00Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12797 Title: High performance pattern matching using bloom-bloomier filter Authors: Tuan N.D.A.; Hieu B.T.; Thinh T.N. Abstract: In this paper, we propose a high performance architecture based on the combination of Bloom Filter and Bloomier Filter (BBF) to enhance the speed of pattern matching process on Clam Antivirus (ClamAV) database. BBF maintains small on-chip memory, low number of fault positives and can indicate which patterns are the candidate matches. The implementation results on low-cost Altera Cyclone II show that our architecture can handle 43,491-characters of ClamAV pattern set with only 9.5 bits per character and achieve a throughput of 1 gigabit per second (Gbps). As compared with previous systems, our memory utilization is far better up to 73%. Fri, 01 Jan 2010 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12797 2010-01-01T00:00:00Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12796 Title: Enhanced FPGA-based architecture for regular expression matching in NIDS Authors: Long L.H.; Hieu T.T.; Tai V.T.; Hung N.H.; Thinh T.N.; Anh Vu D.D. Abstract: Perl Compatible Regular Expression (PCRE) is increasingly used in Network Intrusion Detection System due to its efficiency. However, there are many issues that have not been completely solved for PCRE matching on hardware platform. In this paper, we propose an FPGA-based PCRE matching architecture that effectively improves the constraint repetition, an importance feature of PCRE. We enhance our architecture to handle m flag which is a powerful PCRE modifier. Besides, a toolchain for auto-generating PCRE matching engine is also implemented. Our experimental results on low-cost Altera Cyclone II chip shows that our architecture can achieve throughput up to 1Gbps and save up to 92.74% hardware resource as compared with the conventional architecture. Fri, 01 Jan 2010 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12796 2010-01-01T00:00:00Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12795 Title: Case law and variations in cumulative impact productivity claims Authors: Nguyen L.D.; Ibbs W. Abstract: Proving and quantifying lost productivity due to cumulative impacts of multiple changes are difficult tasks. This paper presents the most acceptable methods from case law and demonstrates their applications for analyzing the loss of productivity. These methods include earned value analysis, measured mile analysis, and combinations of these two. They are either well established or drawn from recent court and board decisions. A case study is used to illustrate and compare the use of these methods. These methods result in considerably different loss of productivity values though the actual amount (i.e., inefficiency in labor hours) is unique for a particular case and though these methods are often thought to be similar or even the same. How a measured mile analysis and its variants are employed affects the amount of lost productivity estimated. The variants can avoid some drawbacks of measured mile and earned value studies. Nevertheless, which method is more accurate and reliable is difficult to provide for a particular claim. Practitioners should choose between them based on the availability of project records and the nature of changes and cumulative impacts. Practitioners may also employ two or more methods to perform a "sensitivity analysis" of the chosen methods and persuade the other party and/or the jury that their estimate of lost productivity is sufficiently certain. © 2010 ASCE. Fri, 01 Jan 2010 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12795 2010-01-01T00:00:00Z