Hasil Pencarian  ::  Simpan CSV :: Kembali

"Dewasa ini proses pembuatan spesifikasi dan verifikasi perangkat lunak kurang begitu diperhatikan. Para pengembang sekarang ini lebih fokus kepada hasil akhir tanpa memperhatikan segala kemungkinan-kemungkinan yang tidak baik di kemudian hari. Proses pembuatan spesifikasi dan verifikasi-lah yang dapat menghindarkan pengguna perangkat lunak akibat kerugian yang akan ditanggungnya saat perangkat lunak tersebut mengalami kerusakan. Kerugian akibat kerusakan ini dibedakan menjadi dua yaitu kerugian langsung akibat rusaknya perangkat lunak tersebut dan kerugian biaya perbaikan perangkat lunak tersebut.Lingu dan LinguSQL adalah suatu jawaban atas kebutuhan dukungan terhadap proses pembuatan spesifikasi dan verifikasi. Lingu yang merupakan bahasa spesifikasi, dapat digunakan untuk spesifikasi perangkat lunak yang dikhususkan pada aplikasi transaksi basis data. Sementara itu, LinguSQL adalah suatu alat verifikasi bahasa Lingu dengan berbantukan theorem prover HOL. Selain melakukan verifikasi LinguSQL juga dapat mentransformasikan bahasa Lingu menjadi bahasa Java.Dalam tugas akhir ini akan digunakan studi kasus aplikasi perbankan dalam melakukan pembuatan spesifikasi dan pelaksanaan verifikasi terhadap perangkat lunak tersebut. Proses pembuatan spesifikasi dan verifikasi ini dijalankan dengan menggunakan Lingu dan LinguSQL. Setelah kegiatan tersebut dilakukan, selanjutnya proses pembuatan spesifikasi dan verifikasi yang dijalankan dengan menggunakan Lingu akan dibandingkan dengan Metode-B. Metode-B adalah bahasa spesifikasi yang sudah umum digunakan dalam melaksanakan proses pembuatan spesifikasi dan verifikasi terhadap perangkat lunak.Hasil dari tugas akhir ini adalah kesimpulan tentang perbandingan antara Lingu dan LinguSQL dengan Metode-B dan Atelier-B. Dalam penelitian ini disimpulkan bahwa Lingu mempunyai fasilitas dukungan terhadap aplikasi basis data. Selain itu, Metode-B didapatkan juga terjamin handal untuk melakukan refinement terhadap suatu perangkat lunak.

---

Nowadays, software specification and verification process is still lacking. Recent developers turn focus more to result without emphasizing any negative possibilities that could be occured next time. However, specification and verification process is able to minimize software failure so that a financial loss caused by either missing functionality or software alteration cost can be reduced.Lingu and Lingu SQL provide support for specification and verification process. Lingu is specification language for database transaction aplication purpose, while LinguSQL is Lingu's verification tool assisted by HOL theorem prover. In addition, LinguSQL transforms Lingu into Java programming language.Research reported here used banking case study. Specification and verification process was run by using Lingu and LinguSQL. Then, result of this process was compared with similar one that had been executed by B-Metode, a previous research by Theresia (2005).This final assignment produces a conclusion of the comparison between Lingu and B-method. Through this research, we conclude that Lingu has a supporting facility for an application that use database. Beside that, we also found that B-method is absolutely reliable for doing refinement on software."

"This festschrift volume, published in honor of Jürgen Dassow on the occasion of his 65th birthday, contains 19 contributions by leading researchers, colleagues, and friends. Covering topics on picture languages, cooperating distributed systems of automata, quantum automata, grammar systems, online computation, word equations, biologically motivated formal systems, controlled derivations, descriptional complexity, as well as 'classical' topics of automata and language theory, the articles presented span the range of the scientific work of Jürgen Dassow."

"This state-of-the-art survey presents the outcome of the 9th Symposium on Formal Methods for Components and Objects, held in Graz, Austria, in November/December 2010. The volume contains 20 revised contributions submitted after the symposium by speakers from each of the following European IST projects: the FP7-IST project AVANTSSAR on automated validation of trust and security of service-oriented architectures; the FP7-IST project DEPLOY on industrial deployment of advanced system engineering methods for high productivity and dependability; the ESF-COST Action IC0701 on formal verification of object-oriented software; the FP7-IST project HATS on highly adaptable and trustworthy software using formal models; the FP7-SST project INESS on an integrated European railway signalling system; the FP7-IST project MADES on a model-driven approach to improve the current practice in the development of embedded systems; the FP7-IST project MOGENTES on model-based generation of tests for dependable embedded systems; as well as the FP7-IST project MULTIFORM on integrated multi-formalism tool support for the design of networked embedded control systems."

"This book constitutes the refereed proceedings of the 15th Brazilian Symposium on Formal Methods, SBMF 2012, held in Natal, Brazil, in September 2012; co-located with CBSoft 2012, the Third Brazilian Conference on Software: Theory and Practice. The 14 revised full papers presented together with 2 keynotes were carefully reviewed and selected from 29 submissions. The papers presented cover a broad range of foundational and methodological issues in formal methods for the design and analysis of software and hardware systems as well as applications in various domains."

"Kourie and Watson advocate an approach known as “correctness-by-construction,” a technique to derive algorithms that relies on formal theory, but that requires such theory to be deployed in a very systematic and pragmatic way. First they provide the key theoretical background (like first-order predicate logic or refinement laws) that is needed to understand and apply the method. They then detail a series of graded examples ranging from binary search to lattice cover graph construction and finite automata minimization in order to show how it can be applied to increasingly complex algorithmic problems. "

"The 15th issue of the Transactions on Computational Science journal, edited by Cong-Vinh Phan, contains six invited papers on autonomic computing, with a special focus on formal engineering methods for nature-inspired computing systems. The papers give an in-depth overview of the area and a comprehensive evaluation of various methodologies for autonomic computing."

"The two-volume set LNCS 7609 and 7610 constitutes the thoroughly refereed proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, held in Heraklion, Crete, Greece, in October 2012. The two volumes contain papers presented in the topical sections on adaptable and evolving software for eternal systems, approaches for mastering change, runtime verification: the application perspective, model-based testing and model inference, learning techniques for software verification and validation, LearnLib tutorial: from finite automata to register interface programs, RERS grey-box challenge 2012, Linux driver verification, bioscientific data processing and modeling, process and data integration in the networked healthcare, timing constraints: theory meets practice, formal methods for the developent and certification of X-by-wire control systems, quantitative modelling and analysis, software aspects of robotic systems, process-oriented geoinformation systems and applications, handling heterogeneity in formal development of HW and SW systems. "

"The two-volume set LNCS 7609 and 7610 constitutes the thoroughly refereed proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, held in Heraklion, Crete, Greece, in October 2012. The two volumes contain papers presented in the topical sections on adaptable and evolving software for eternal systems, approaches for mastering change, runtime verification: the application perspective, model-based testing and model inference, learning techniques for software verification and validation, LearnLib tutorial: from finite automata to register interface programs, RERS grey-box challenge 2012, Linux driver verification, bioscientific data processing and modeling, process and data integration in the networked healthcare, timing constraints: theory meets practice, formal methods for the developent and certification of X-by-wire control systems, quantitative modelling and analysis, software aspects of robotic systems, process-oriented geoinformation systems and applications, handling heterogeneity in formal development of HW and SW systems. "

"This book constitutes the refereed proceedings of the 9th International Conference on Integrated Formal Methods, IFM 2012, held Pisa, Italy, in June 2012. The 20 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 59 submissions. The papers cover the spectrum of integrated formal methods, ranging from formal and semiformal notations, semantics, proof frameworks, refinement, verification, timed systems, as well as tools and case studies."

"This book constitutes the thoroughly refereed post-proceedings of the 8th International Workshop on Web Services and Formal Methods, WS-FM 2011, held in Clermont-Ferrand, France, in September 2011. The workshop was co-located with the 9th International Conference on Business Process Management, BPM 2011. The 9 full papers presented were carefully reviewed and selected from 14 submissions. They deal with service oriented computing (SOC), cloud computing and formal methods."