Metode Formal

Mengapa seorang software engineers PERLU memiliki kemampuan matematika yang mumpuni? Pertanyaan ini seringkali ditanyakan oleh mahasiswa jurusan informatika dan masyarakat umum. Sepertinya telah terjadi salah-pemahaman mengenai keilmuan Informatika itu sendiri. Masyarakat awam "memiliki" pemahaman bahwa informatika terkait dengan Facebook, Twitter dan Internet Marketing, sedangkan mahasiswa informatika sering memahami keilmuan informatikan itu sebagai Gaming dengan berbagai bentuknya. Semua itu merupakan pandangan yang keliru.

Beberapa waktu lalu saya telah menulis tentang kemampuan matematika dasar yang harus dimiliki oleh seorang software engineer. Tulisan itu dapat dibaca pada link ini:

http://stanleykarouw.blogspot.com/2012/06/matematika-dasar-untuk-software.html

Pada bagian ini, saya akan menulis tentang Formal Methods atau Metode Formal. Sebagai pengantar, maka perlulah dikemukakan apa itu formal methods tersebut ...

Formal methods is the term applied to the analysis of software (and computer hardware) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include denotational semantics, axiomatic semantics, operational semantics, and abstract interpretation.

Jika diterjemahkan maka akan seperti ini:

Metode formal adalah istilah yang diterapkan pada analisis perangkat lunak (dan perangkat keras komputer) yang hasilnya diperoleh murni melalui penggunaan metode matematika ketat. Teknik-teknik matematika yang digunakan meliputi semantik denotational, semantik aksiomatik, semantik operasional, dan interpretasi abstrak.

Formal Methods merupakan bagian pembahasan pengembangan perangkat lunak yang makin berkembang sekarang ini. Mahasiswa jurusan informatika harus memahami konsep dan implementasi Formal Methods dalam pengembangan perangkat lunak, dan untuk itu dibutuhkan kemampuan matematika dasar dan lanjut yang menyeluruh.

Misalnya kita dapat melihat apa yang dimaksud dengan interpretasi abstrak:

Abstract interpretation models the effect that every statement has on the state of an abstract machine (i.e., it 'executes' the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviours of the system: the abstract system is thus made simpler to analyze, at the expense of incompleteness (not every property true of the original system is true of the abstract system).
Use of assertions in program code as first suggested by Hoare logic. There is tool support for some programming languages (e.g., the SPARK programming language (a subset of Ada) and the Java Modeling Language — JML — using ESC/Java and ESC/Java2, Frama-c WP (weakest precondition) plugin for the C language extended with ACSL (ANSI/ISO C Specification Language).

atau dalam terjemahannya ...

Interpretasi abstrak memodelkan efek dari setiap pernyataan pada keadaan mesin abstrak (yaitu, 'mengeksekusi' perangkat lunak berdasarkan sifat matematis dari setiap pernyataan dan deklarasi). Mesin abstrak memperkirakan perilaku sistem: sehingga dapat digunakan untuk menganalisis, dengan model sistem yang tidak lengkap (yakni tidak setiap properti dari sistem yang asli dimodelkan pada sistem abstrak). 

Penggunaan pernyataan dalam kode program sebagai pertama kali diusulkan oleh logika Hoare. Ada alat dukungan untuk beberapa bahasa pemrograman (misalnya, pemrograman SPARK bahasa (subset dari Ada) dan Modeling Language Jawa - JML - menggunakan ESC / Jawa dan ESC/Java2, Frama-c WP (prasyarat paling lemah) plugin untuk C bahasa diperpanjang dengan ACSL (ANSI / ISO C Language Specification)).

Matematika Diskrit adalah salah satu mata kuliah yang mendasari konsep-konsep metode formal. Sedangkan Kalkulus, Aljabar Linier, Probabilitas dan Statistik serta Metode Numerik memberikan latar belakang keteknikan untuk formulasi permasalahan, pemodelan masalah dan penyusunan algoritma penyelesaian masalah, untuk selanjutnya disalin dalam bahasa coding.

Berikut ini adalah slide kuliah tentang Formal Method:

https://docs.google.com/open?id=0BxSxy7HfW5oJMGFqMHljQjBMNnM

Beberapa rujukan untuk studi awal tentang Formal Method:
http://en.wikipedia.org/wiki/Denotational_semantics
http://en.wikipedia.org/wiki/Hoare_logic
http://en.wikipedia.org/wiki/Operational_semantics
http://en.wikipedia.org/wiki/Abstract_interpretation

Security and Privacy Requirements

Security dan Privacy Requirements sering diklasifikan sebagai non-fungsional requirements dalam pengembangan perangkat lunak. Namun, seiring dengan perkembangan perangkat lunak yang menuju pada tren Komputasi Awan, maka requirements yang berhubungan dengan security dan privacy menjadi kian diperhitungkan oleh user dan stakeholders pemilik perangkat lunak.

Berikut ini adalah non fungsional requirements terkait high-level security dan privacy dalam aplikasi e-voting (Pemilihan Online):

1) Eligibility (atau kelayakan); yang dimaksud dengan kelayakan dalam aplikasi e-voting adalah pemilih yang layak dapat diidentifikasi dengan akurat dan terdaftar dengan baik. Eligibility dalam aplikasi e-voting diartikan juga sebagai hanya pemilih yang terdaftar yang dapat mengeksekusi proses voting pada e;ection server.
2) Uniqeness (atau keunikan); yang dimaksud dengan keunikan disini adalah aktor pemilih hanya diberikan satu kali kesempatan mengeksekusi proses pemilihan, setelah "hak satu kali" dikonfirmasi, maka aktor pemilih tidak bisa lagi melakukan proses pemilihan. Tentu saja, akan terdapat skenario jika aktor pemilih, memilih beberapa kali, maka sistem hanya akan mendaftarkan pilihan voter yang terakhir saja.
3) Accuracy (atau keakuratan); yang dimaksud dengan persyaratan keakuratan adalah semua hasil pemilihan yang telah dilakukan harus dapat dihitung dengan tepat. Tidak ada yang dapat mengubah, menghapus, membatalkan, menggandakan semua hasil pemilihan.
4) Soundness (atau kukuh); yakni invalid votes (atau pemilih yang gagal melakukan prosedur pemilihan) tidak akan dihitung. Misalnya hasil pemilihan yang menunjukkan format yang keliru atau content yang keliru. Kasus yang dapat dicontohkan adalah hanya ada 1, 2 dan 3 kemungkinan pilih, tapi yang keluar angka selain dari 1, 2 dan 3.
5) Privacy (atau kerahasiaan); persyaratan non fungsional ini terkait dengan kerahasiaan identitas aktor pemilih dan ketidakmungkinan untuk menghubungkan identitas aktor pemilih dengan hasil pemilihan tertentu.
6) Fairness (atau keseragaman); yang dimaksud dengan fairness adalah semua aktor pemilih harus dapat melihat hasil akhir pemilihan pada waktu yang sama. Tidak boleh ada yang mendahului ataupun ketinggalan.
7) Transparency (atau keterbukaan); yakni data yang terkait dengan sistem informasi pemilihan dan content hasil pemilihan harus available untuk semua stakeholder. Termasuk source code aplikasi, yang harus dapat direview oleh siapa saja.
8) Robustness (atau kekuatan); yang dimaksud dengan robustness adalah tidak ada aktor stakeholders yang dapat mempengaruhi proses voting yang dilakukan aplikasi, dimulai pada proses masukan hingga keluaran dari sistem aplikasi.
9) Uncoercibility; yang dimaksud dengan requirement ini adalah seorang coercer tidak dimungkinkan untuk dapat mempengaruhi (memaksa) aktor voter untuk mengubah hasil pemilihan yang telah dihitung oleh sistem aplikasi
10) Receipt-freeness; untuk mencegah jual-beli suara, maka semua aktor voter tidak diizinkan untuk mendapatkan nota tercetak yang menunjukkan content hasil pemilihan aktor pemilih.
11) Verifiability; yakni setiap aktor pemilih dapat memeriksa bahwa infrastuktur sistem informasi telah menerima dengan tepat hasil pilihan dan telah menghitung pilihan aktor pemilih (ini yang disebut personal verifiability); dan pada saat yang bersamaan juga dapat mengkonfirmasi semua user tentang hasil perhitungan (ini disebut universal verifiability).

References:
1. M. Volkamer, Evaluation of Electronic Voting, Springer - 2009.
2. R. Celeste, D. Thornburgh and H. Lin, Asking the Right Questions about Electronic Voting, National Academies Press - 2006

SOSE: Service-oriented Software Engineering

Konsep SOSE atau Service Oriented Software Engineering, secara kasar dapat dianggap sebagai "penggabungan" antara software sebagai services (layanan) dengan komputasi awam (atau cloud computing). 

Konsep ini pertama kali disebut oleh 

1) Stephen S. Yau is the director of Arizona State Univer- sity’s Information Assurance Center and a professor of computer science. His research interests include software engineering, cybersecurity, distributed computing systems, service-based computing, and cloud computing systems. Yau received a PhD in electrical engineering from the Uni- versity of Illinois at Urbana-Champaign. He is a Life Fellow of IEEE and a Fellow of the American Association for the Advancement of Science. Contact him at yau@asu.edu orhere .

2) Ho G. An is a PhD student in the School of Computing, Informatics and Decision System Engineering at Arizona State University. His research interests include services and cloud computing, security, and privacy. An received an MS in computer science from Arizona State University. Contact him at ho.an@asu.edu.

(Gambar diambil dari http://www.infoq.com/articles/ieee-software-engineeering-services-cloud-computing)

Seperti yang kita ketahui bersama, perkembangan service oriented architecture dan cloud computing menjadi sangat pesat belakangan ini, terlebih khusus dalam area industri dan akademisi, memicu berkembangnya aplikasi ber-skala besar yang ditujukan untuk pengembangan penelitian kolaboratif di berbagai bidang seperti: e-bisnis, kesehatan, aplikasi grid computing, infrastruktur komputasi perusahaan2, aplikasi2 untuk militer dan keamanan. Kedua paradigma software development tersebut diatas telah membuat lebih mudah dan lebih ekonomis untuk membuat segala sesuatu dari perangkat lunak komersial yang sederhana hingga sistem informasi yang kompleks, termasuk "killer application" yang bersifat mission-critical.

Pada hakikatnya kedua konsep paradigma pengembangan software memiliki "kemiripan" dalam hal oursourcing sumber daya dan transfer pengelolaan TI untuk layanan aplikasi, meskipun demikian terdapat perbedaan yang mencolok dalam hal "paradigma software engineering". Komputasi Service-Oriented berfokus pada desain arsitektur yang memungkinkan pengembangan aplikasi melalui penemuan layanan dan komposisi sedangkan cloud computing berfokus pada pengiriman efektif layanan kepada pengguna melalui virtualisasi sumber daya fleksibel dan scalable dan load balancing.

Konsep SOSE atau Service Oriented Software Engineering mencoba untuk "menggabungkan" keunggulan dan "mereduksi" perbedaan kedua paradigma tersebut. Melalui SOSE, dioptimalkan konsep arsitektur berorientasi layanan (SOA) yang memberikan gaya arsitektur, protokol standar, dan interface yang diperlukan untuk pengembangan aplikasi, dan Cloud Computing memberikan layanan yang diperlukan untuk pengguna melalui virtualisasi dan sumber daya penyatuan. Menggabungkan layanan dan komputasi awan dalam kerangka rekayasa perangkat lunak dapat membantu pengembang aplikasi dan penyedia layanan memenuhi tantangan individu paradigma masing-masing.

(Gambar diambil dari http://www.infoq.com/articles/ieee-software-engineeering-services-cloud-computing)

Meskipun SOSE secara konseptual menjanjikan, realisasinya akan memerlukan penelitian tambahan dalam rekayasa perangkat lunak untuk menghadapi tantangan, seperti keamanan dan kualitas-of-service (QoS) manajemen yang muncul dalam layanan atau komputasi awan.

Visi dari SOSE dapat dilihat pada Gambar berikut ini:

(Gambar diambil dari http://www.infoq.com/articles/ieee-software-engineeering-services-cloud-computing) 

Keterangan selanjutnya dapat diperoleh di:

http://www.infoq.com/articles/ieee-software-engineeering-services-cloud-computing

dan 

http://www.computer.org/portal/web/computingnow/computer

References dari Sumber Kutipan:

1. Y. Chen and W.-T. Tsai, Service-Oriented Computing and Web Data Management: From Principles to Development, Kendall Hunt, 2010.
2. K. Channabasavaiah, E. Tuggle, and K. Holley, “Migrat­ing to a Service-Oriented Architecture,” 16 Dec. 2003.
3. S.S. Yau and H.G. An, “Confidentiality Protection in Cloud Computing Systems,” Int’l J. Software Informatics, vol. 4, no. 4, 2010, pp. 351-365.
4. Y. Zhu et al., “Dynamic Audit Services for Outsourced Storage in Clouds,” to be published in IEEE Trans. Services Computing, 2011.
5. L. Whitney, “Amazon EC2 Cloud Service Hit by Botnet, Outage,” CNET News, 11 Dec. 2009.
6. “Google Cloud Platform Used for Botnet Control,” Info Security, 10 Nov. 2009.
7. C. Li, A. Raghunathan, and N. Jha, “Secure Virtual Machine Execution under an Untrusted Management OS,” Proc. IEEE 3rd Int’l Conf. Cloud Computing (CLOUD 10), IEEE CS Press, 2010, pp. 172-179.
8. Cloud Security Alliance, “Top Threats to Cloud Computing V1.0,” Mar. 2010.
9. S.S. Yau et al., “Automated Situation-Aware Service Composition in Service-Oriented Computing,” Int’l J. Web Services Research, vol. 4, no. 4, 2007, pp. 59-82.
10. S.S. Yau et al., “Rapid Development of Adaptable Situation- Aware Service-Based Systems,” Web Services Research for Emerging Applications: Discoveries and Trends, L.-J. Zhang, ed., Information Science Reference, IGI Global, 2010, pp. 104-139.
11. S.S. Yau et al., “Toward Development of Adaptive Service- Based Software Systems,” IEEE Trans. Services Computing, vol. 2, no. 3, 2009, pp. 247-260.
12. B.T. Ward and J.C. Sipior, “The Internet Jurisdiction Risk of Cloud Computing,” Information Systems Management, vol. 27, no. 4, 2010, pp. 334-339.

Mekanisme Configured Tunneling

Tunneling menyediakan sebuah cara untuk memanfaatkan infrastruktur routing IPv4 yang telah ada untuk membawa traffic IPv6. Host dan router IPv6/IPv4 dapat mengirimkan datagram IPv6 melalui topologi routing IPv4 dengan mengenkapsulasi datagram IPv6 tersebut kedalam paket IPv4. Tunneling dapat digunakan dalam berbagai macam cara:

• Router-to-Router: Router IPv6/IPv4 yang saling terhubung oleh sebuah infrastruktur IPv4 dapat menggunakan tunnel untuk melewatkan paket IPv6 diantara mereka. Dalam hal ini, tunnel merupakan satu segmen jaringan dari end-to-end jalur yang dilalui oleh paket IPv6.

• Host-to-Router: Host IPv6/IPv4 dapat men-tunnel paket IPv6 ke sebuah intermediary router IPv6/IPv4 yang dapat dicapai melalui sebuah infrastruktur IPv4.

• Host-to-Host: Host IPv6/IPv4 yang terhubung melalui sebuah infrastruktur IPv4 dapat men-tunnel paket IPv6 diantara keduanya.

• Router-to-Host: Router IPv6/IPv4 dapat men-tunnel paket IPv4 ke tujuan host IPv6/IPv4. Tunnel ini berada pada segmen terakhir dari jalur.

Configured Tunneling dapat digunakan pada semua kondisi diatas tetapi kebanyakan digunakan pada Router-to-Router karena membutuhkan konfigurasi secara eksplisit terhadap tunneling endpoint.

Mekanisme yang menjadi pokok dari tunneling adalah

• Bagian dimana paket IPv6 memasuki tunnel (entry node [encapsulator]) membuat sebuah header IPv4 yang mengenkapsulasi paket dan mengirimkannya.
• Bagian ujung dari tunnel (exit node [decapsulator]) menerima paket yang terenkapsulasi tersebut kemudian menyusun kembali paket tersebut bila diperlukan, menghapus header IPv4, lalu memproses paket IPv6 yang diterima.
• Encapsulator dapat mungkin perlu memelihara soft-state information dari setiap tunnel seperti parameter sebagai MTU tunnel untuk memproses paket IPv6 yang diteruskan kedalam tunnel.

Enkapsulasi

Enkapsulasi dari sebuah datagram IPv6 didalam IPv4 adalah sebagai berikut

Gambar Peng-engkapsulasi-an datagram IPv6 dalam IPv4 (Sumber: Nordmark et al, 2005)

Dekapsulasi

Saat sebuah host atau router IPv6/IPv4 menerima sebuah datagram IPv4 yang ditujukan ke alamat IPv4 node tersebut atau ke sebuah alamat multicast dan field Protocol pada paket tersebut bernilai 41 maka sangat mungkin itu merupakan sebuah tunnel packet dan perlu diverifikasi apakah termasuk pada salah satu dari tunnel yang telah dikonfigurasi dengan memeriksa alamat sumber/tujuan, menyusun kembali (reassembly) apabila terfragmentasi, dan menghapus header IPv4. Decapsulator harus memastikan keabsahan alamat sumber tunnel sebelum memproses paket lebih jauh untuk mengurangi masalah dengan address spoofing. Pengecekan ini juga berlaku terhadap paket yang diarahkan kepada protokol transport dari decapsulator. Paket dengan alamat IPv4 sumber yang tidak sesuai harus dibuang dan decapsulator menciptakan pesan kesalahan ICMP. Efek samping dari verifikasi alamat ini adalah node akan membuang secara diam-diam paket dengan alamat sumber yang salah serta paket yang diterima oleh node tetapi tidak ditujukan secara langsung kepadanya (contohnya paket ke alamat broadcast).

Decapsulator harus memiliki IPv6 MRU paling kurang 1500 byte pada tunnel interface dan MTU IPv6 terbesar pada interface IPv6. Decapsulator juga harus dapat menyusun kembali (reassembly) paket IPv4 yang sesudah disusun kembali, maksimum berukuran 1500 byte. Jumlah 1500 byte merupakan dihasilkan oleh encapsulator yang menggunakan skema MTU statis, sedangkan untuk encapsulator yang menggunakan skema MTU dinamis dapat menyebabkan ukuran paket melebihi MTU terbesar pada interface decapsulator. Batasan terhadap reassembly ini membuat penentuan MTU tunnel secara dinamis oleh encapsulator dapat memanfaatkan MTU jalur IPv4 yang lebih besar. Decapsulator menyusun ulang paket IPv4 sebelum melakukan dekapsulasi. Dekapsulasi ditunjukkan sebagai berikut

Gambar Pendekapsulasian IPv6 dari IPv4 (Sumber: Nordmark et al, 2005)

Setelah melakukan dekapsulasi, decapsulator harus menghapus paket dengan alamat IPv6 sumber yang tidak valid yakni:

• Alamat multicast (FF00::/8)
• Alamat loopback (::1)
• IPv4-compatible IPv6 Address (::/96).
• Seluruh IPv4-mapped IPv6 address (::ffff:0:0/96)

Secara logis, maka prosedur tunneling dapat menggunakan beberapa algoritma. Pada dasarnya teknik tunneling dapat digunakan untuk implementasi pada arsitektur jaringan yang memiliki IPv4 dan IPv6.

Information Technology & Christian Scholars Paradigms

Remarks for discussions on IT and Christian Scholars Paradigm

1) de omnibus dubitandum; cor ad cor loquitor [1]

2) christian scholars framework for seeing

3) Relation of Science, Knowledge and Technology

1. Keinginan untuk menyelidiki sesuatu
2. Pengamatan Awal akan melahirkan gagasan (termasuk paradigma)
3. Perencanaan suatu proses penelitian terpadu
4. Hasil Penelitian dirangkum, diklasifikasikan (melalui proses analisis dan disain)
5. Menemukan inter-relasi antara beberapa vektor
6. Menerapkan/Memanfaatkan "penemuan" baru --> Inilah yang dimaksud dgn TEKNOLOGI
7. Memberikan interpretasi, arti dan makna.

4) Methodology Contradictions:

Segala Sesuatu harus dapat dimengerti berdasarkan urutan peristiwa sebab-akibat dalam sistem tertutup

Contoh Kontradiksi Metodologis:
Hukum Termodinamika I, II dan III
1. Jumlah energi itu konstan (tidak berubah) [energi tidak diciptakan dan tidak dapat dimusnahkan]
2. Potensi alam serta isinya (cenderung) merosot [entropi]
3. Keadaan Lampau tidak terpulihkan

5) Christian Scholar Paradigm:

Segala Sesuatu dapat dimengerti berdasarkan urutan peristiwa sebab-akibat dalam sistem terbuka

Implementasi:
Entropi (penyusutan) adalah ungkapan lain dari upah dosa adalah maut dan kedagingan [2]
Harus ada ex-nihilo untuk "memulai" segala sesuatu (lihat Gambar dibawah)
Adanya sistem-terbuka dalam sejarah bumi (Misalnya peristiwa Kain da Habel [3], peristiwa Air Bah [4] , peristiwa Menara Babel [5], peristiwa kelahiran Yesus Kristus [6], peristiwa Guttenberg [7] dan akhirnya peristiwa "kemunculan" Web 2.0[8])

6) IT Spectrum

7) Conclusion

dapat digambarkan dengan [8]:

dengan S adalah "panjang" daur hidup manusia dalam garis waktu

Kutipan:

1. Ulangan 6:5

2. Roma 6:23

3. Kejadian 4:22

4. Kejadian 7

5. Kejadian 10-11

6. Lukas 2

7. Pengkotbah 1:9-10

8. Kitab Roma 8