http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/12 Mon, 18 May 2026 07:29:53 GMT 2026-05-18T07:29:53Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/2369 Title: Nghiên cứu về chứng minh tự động (Theorem Proving) trong CafeOBJ Authors: Tạ Thị Thu, Hiền Abstract: Đặc tả và kiểm chứng là một trong những giải pháp quan trọng nhằm nâng cao chất lượng phần mềm. Có hai kĩ thuật được sử dụng phổ biến nhất hiện nay là kiểm chứng mô hình (Model Checking) và chứng minh tự động (Theorem Proving). Khác với kiểm chứng mô hình, chứng minh tự động có thể kiểm chứng với mô hình vô hạn trạng thái. CafeOBJ là một ngôn ngữ hỗ trợ đặc tả và kiểm chứng theo tư tưởng của chứng minh tự động. Mục tiêu của luận văn là nắm bắt và sử dụng cafeOBJ để đặc tả và kiểm chứng một số hệ thống điển hình trong thực tiễn. Luận văn đã đạt được các kết quả sau: - Tìm hiểu và nắm rõ phương pháp đặc tả phần mềm sử dụng ngôn ngữ đại số CafeOBJ. - Nắm vững phương pháp chứng minh tự động sử dụng tư tưởng qui nạp toán học để kiểm chứng các thuộc tính bất biến (invariant property). Với phương pháp này, để chứng minh một thuộc tính bất biến, chúng ta cần chứng minh nó đúng tại trạng thái khởi tạo của hệ thống. Giả sử thuộc tính đúng tại một trạng thái bất kỳ s, chúng ta phải chứng minh nó đúng với mọi trạng thái tiếp theo của s. - Áp dụng những kiến thức đã tìm hiểu để kiểm chứng 04 thuộc tính của hệ thống đa tác tử. Trong hệ thống này, các tác tử chia sẻ một tài nguyên dùng chung. Số lượng tác tử trong hệ thống là vô hạn vì vậy không gian trang thái là vô hạn. Với hệ thống này, chúng ta không thể áp dụng các phương pháp kiểm chứng mô hình vì lý do trên. Kết quả kiểm chứng cho thấy hệ thống đa tác tử thỏa mãn các thuộc tính cần kiểm tra tại mọi trạng thái của hệ thống. Description: Đặc tả và kiểm chứng là một trong những giải pháp quan trọng nhằm nâng cao chất lượng phần mềm. Có hai kĩ thuật được sử dụng phổ biến nhất hiện nay là kiểm chứng mô hình (Model Checking) và chứng minh tự động (Theorem Proving). Khác với kiểm chứng mô hình, chứng minh tự động có thể kiểm chứng với mô hình vô hạn trạng thái. CafeOBJ là một ngôn ngữ hỗ trợ đặc tả và kiểm chứng theo tư tưởng của chứng minh tự động. Mục tiêu của luận văn là nắm bắt và sử dụng cafeOBJ để đặc tả và kiểm chứng một số hệ thống điển hình trong thực tiễn. Luận văn đã đạt được các kết quả sau: - Tìm hiểu và nắm rõ phương pháp đặc tả phần mềm sử dụng ngôn ngữ đại số CafeOBJ. - Nắm vững phương pháp chứng minh tự động sử dụng tư tưởng qui nạp toán học để kiểm chứng các thuộc tính bất biến (invariant property). Với phương pháp này, để chứng minh một thuộc tính bất biến, chúng ta cần chứng minh nó đúng tại trạng thái khởi tạo của hệ thống. Giả sử thuộc tính đúng tại một trạng thái bất kỳ s, chúng ta phải chứng minh nó đúng với mọi trạng thái tiếp theo của s. - Áp dụng những kiến thức đã tìm hiểu để kiểm chứng 04 thuộc tính của hệ thống đa tác tử. Trong hệ thống này, các tác tử chia sẻ một tài nguyên dùng chung. Số lượng tác tử trong hệ thống là vô hạn vì vậy không gian trang thái là vô hạn. Với hệ thống này, chúng ta không thể áp dụng các phương pháp kiểm chứng mô hình vì lý do trên. Kết quả kiểm chứng cho thấy hệ thống đa tác tử thỏa mãn các thuộc tính cần kiểm tra tại mọi trạng thái của hệ thống. Fri, 01 Jan 2010 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/2369 2010-01-01T00:00:00Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/32 Title: Metamagnetism, giant magnetoresistance and magnetocaloric effects in RCo2-based compounds in the vicinity of the Curie temperature Authors: Nguyen, Huu Duc; D.T., Kim Anh; P.E., Brommer Abstract: Magnetisation and magnetoresistance isotherms were measured for a number of (R,R′)Co2, (R,Y)Co2 and R(Co,Si)2 (R,R′ = rare earth) compounds. A metamagnetic transition is observed just above the Curie temperature (TC) of compounds having a first order phase transition, i.e. ErCo2-, HoCo2-, and DyCo2-based ones. Both 4f- and 3d-sublattice magnetic moments contribute to a sharp change of the magnetisation at this transition. The concurring suppression of the magnetoresistance can be considered to be due to quenching of spin fluctuations. In addition, the magnetic entropy change ΔSm is estimated from the magnetisation data by using a Maxwell equation. The resulting giant magnetocaloric effects are discussed in terms of the 4fR-localised spin and the 3d(Co)-spin fluctuations as well as the nature of the phase transition. Tue, 01 Jan 2002 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/32 2002-01-01T00:00:00Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/31 Title: Unconventional GMR angular dependence using a compensated ferrimagnet Authors: N.T., Nam; L., Ranno Abstract: We have designed a GdCo/Cu/NiFe Giant Magnetoresistance (GMR) trilayer, the magnetoresistance of which does not always depend on the angle between the magnetisations of the electrodes. Using a GdCo ferrimagnetic alloy close to compensation, it was possible to experimentally reach the spin flop field Bsf of the ferrimagnetic layer. Below Bsf , the ferrimagnetic layer behaves as a ferromagnetic layer, however above Bsf,the ferrimagnetic sublattice magnetisations are no longer antiparallel and rotate 90◦ away from the GdCo layer total magnetisation, i.e. 90◦ away from the applied field. The GMR responds to the angle between Co and NiFe magnetisations and not to the angle between GdCo and NiFe magnetisations. Such a structure allows to study the change of sign of the GdCo spin polarisation as a function of temperature, and details of the GdCo magnetisation when usual magnetometry is difficult. FeNi can be seen as a sensor for the in-plane component of Co sublattice magnetisation, whereas extraordinary Hall effect measurements give a complementary image of the perpendicular component of the Co magnetisation. Tue, 01 Jan 2008 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/31 2008-01-01T00:00:00Z http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/25 Title: Magnetic sensors based on piezoelectric–magnetostrictive composites Authors: Nguyen, Huu Duc; D.T., Huong Giang Abstract: Magnetoelectric (ME) composites have been fabricated by sandwiching a lead titanate (PZT) laminate between two magnetostrictive (Tb(Fe0.55Co0.45)1.5) (known as Terfecohan) films. Giant ME effect at low fields obtained is associated to large magnetostriction as well as high magnetostrictive susceptibility of the Terfecohan films. Magnetoelectric voltage coefficients, αE = (∂E/∂H), as large as 3350 and 9650Vm/kAm were achieved, respectively, for the as-deposited, and annealed films. The coefficient αE was, however, highly dependent on the direction of the magnetic field with respect to the electrical polarization. On the basic of this magnetoelectric composite, a magnetic sensor operating in an ac magnetic field of 0.1mT at a resonant frequency of 40Hz has been prepared. The ME voltage response in applied magnetic fields (dVME/dH) as large as 130 mV/mT was obtained. Tue, 01 Jan 2008 00:00:00 GMT http://tainguyenso.vnu.edu.vn/jspui/handle/123456789/25 2008-01-01T00:00:00Z