คำสำคัญ

(static)
�� อาจใช้ Tool ช่วยตรวจวิเคราะห์ เอกสารและโปรแกรม code
(dynamic)
�� ใช้ข้อมูลทดสอบระบบและสังเกตผลการทำงาน

event-based อันนี้อาจารย์ ดร.อุษา อธิบายซะเข้าใจเลย
คือเกิดเหตุการณ์ตามเงื่อนไขก่อนค่อยทำ ไม่ต้องเช็คทุกครั้งว่ามีการเปลี่ยนแปลงอะไรไปบ้าง

state-based งงอยู่นาน..ตอนนี้จะงงต่อไปรึป่าว
คือเช็คในเวลาที่มีการเปลี่ยนสถานะ

False Positive
เกิดขึ้นเมื่อระบบได้ระบุว่าการกระทำหนึ่งเป็นการบุกรุกแต่ที่แท้แล้วไม่ใช่

<< เอาไว้ศึกษาก่อนเรียน >>

Common types of computer bugs

* Conceptual error (code is syntactically correct, but the programmer or designer intended it to do something else)

# Maths bugs

* Division by zero
* Arithmetic overflow or underflow
* Loss of arithmetic precision due to rounding or numerically unstable algorithms

# Logic bugs

* Infinite loops and infinite recursion

# Syntax bugs

* Use of the wrong operator, such as performing assignment instead of equality test. In simple cases often warned by the compiler; in many languages, deliberately guarded against by language syntax

# Resource bugs

* Null pointer dereference
* Using an uninitialized variable
* Off by one error, counting one too many or too few when looping
* Access violations
* Resource leaks, where a finite system resource such as memory or file handles are exhausted by repeated allocation without release.
* Buffer overflow, in which a program tries to store data past the end of allocated storage. This may or may not lead to an access violation. These bugs can form a security vulnerability.
* Excessive recursion which though logically valid causes stack overflow

#Co-programming bugs

* Deadlock
* Race condition
* Concurrency errors in Critical sections, Mutual exclusions and other features of concurrent processing. Time-of-check-to-time-of-use (TOCTOU) is a form of unprotected critical section.

# Teamworking bugs

* Unpropagated updates; e.g. programmer changes "myAdd" but forgets to change "mySubtract", which uses the same algorithm. These errors are mitigated by the Don't Repeat Yourself philosophy.
* Comments out of date or incorrect: many programmers assume the comments accurately describe the code
* Differences between documentation and the actual product

[[อ่านที่นี่]]

survey paper

ทำการ survey paper ทั้งที .. ตอนแรกก็กะว่าจะสำรวจสัก 3-4 paper

มันก็จริงอยู่หรอก ทำไปทำมา .. มันก็ต้องดู paper อื่น ๆ วุ่นวายไปหมด
เพื่อจะหาความหมายของ Keyword บ้าง รึเพื่อจะเข้าใจสูตร rules ต่างๆ
อีกทั้งยังต้องอ่านบทความหรือแม้แต่หาความรู้จากเว็บทั้งหลายแหล่
อะไรต่อมิอะไรมากมายเลยทีเดียว เริ่มจะเก่งภาษาขึ้นบ้างแล้วนะเนี่ย
แต่ก็เพื่อให้เข้าใจ paper ที่เลือกมา survey ให้มากที่สุด .....เหนื่อยจริง ๆ T_T

+ Rule-Based Runtime Verification (2004) :: อันนี้ survey
+ Event-based runtime verification of Java programs (2005) :: อันนี้ survey
+ Rule systems for run-time monitoring: from Eagle to RuleR (2007) :: อ่านประกอบ

+ Calysto: Scalable and Precise Extended Static Checking (2008) :: อันนี้ survey (แหม อันนี้เกือบใหม่ ..ภูมิใจจัง)

symbolic execution

http://www.youtube.com/watch?v=azTVEwxN8zM&hl=th

LLVM

LLVM หรือชื่อเต็มๆ ว่า Low Level Virtual Machine ซึ่งเป็นสถาปัตยกรรม/เทคโนโลยีการแปลง code ในระดับล่างจริงๆ โดยโปรเจคนี้เริ่มต้นที่มหาวิทยาลัย Illinois และ Apple เข้ามาให้การสนับสนุนในการช่วยพัฒนามาตั้งแต่ปี 2005 และได้เริ่มใช้งานใน Leopard ในการช่วยแปลง code ทาง graphics สำหรับเครื่องแมคฯ รุ่นต่ำๆ ที่ไม่มี hardware เฉพาะทาง

LLVM compiler อาจจะเข้ามาเป็นส่วนหนึ่งของ Xcode ในอนาคตอันใกล้นี้ และอาจจะแทน GCC แบบสมบูรณ์แบบด้วย

ซึ่งผลของการใช้ LLVM นี้จะช่วยให้นักพัฒนาทำงานได้ง่ายขึ้น และโปรแกรมที่รันเร็วขึ้น "มาก" (ราคาคุยหรือเปล่าไม่รู้) ในฮาร์ดแวร์เดียวกัน

GCs (cont.)

อ่านอันนี้เข้าใจขึ้น http://en.wikipedia.org/wiki/Guarded_Command_Language

In pseudocode:

if a < b then c := True
else c := False

In guarded command language:

if a < b c := true
[] a ≥ b c := false
fi

Skip and Abort
Skip and Abort are very simple as well as important statements in the guarded command language. Abort is the undefined instruction: do anything. The abort statement does not even need to terminate. It is used to describe the program when formulating a proof, in which case the proof usually fails. Skip is the empty instruction: do nothing. It is used in the program itself, when the syntax requires a statement, but the programmer does not want the machine to change states.

Guarded Command

Guarded Commands
• Suggested by Dijkstra ปี 1975
• Purpose: to support a new programming methodology that supported verification (correctness) during development
• Basis for two linguistic mechanisms for concurrent programming (in CSP and Ada)
• Basic Idea: if the order of evaluation is not important, the program should not specify one

Selection Guarded Command
• Form
if ->
[] ->
...
[] ->
fi
fi เป็นการจบด้วยการ reverse word
• Semantics: when construct is reached,
– Evaluate all Boolean expressions
– If more than one are true, choose one non-deterministically
– If none are true, it is a runtime error (ถ้าเป็น false ทั้งหมดจะเกิด runtime eror)

If I = 0 - > sum := sum +i
[] i > j - > sum := sum + j
[] j >I - > sum := sum +i

*ถ้า if = 0 และ j > I โครงสร้างจะเลือก nondeterminate ระหว่างการกำหนดค่าที่ 1 กับ 3


Loop Guarded Command
• Form
do ->
[] ->
...
[] ->
od
• Semantics: for each iteration
– Evaluate all Boolean expressions
– If more than one are true, choose one non-deterministically; then start loop again
– If none are true, exit loop



Guarded Commands: Rationale
• Connection between control statements and program verification is intimate
• Verification is impossible with goto statements
• Verification is possible with only selection and logical pretest loops
• Verification is relatively simple with only guarded commands


อันนี้อ่านแล้วยังงง ๆ ไว้อ่านใหม่ :
http://www.ipl.t.u-tokyo.ac.jp/~hu/pub/teach/msp06/lec2.pdf

KU 2009

insert image testing.

photo by Ms.Usa Sammapun

first blog

....................