ในวิทยาการคอมพิวเตอร์การวิเคราะห์โปรแกรมแบบคงที่ (หรือที่รู้จักกันในชื่อการวิเคราะห์แบบคงที่หรือการจำลองแบบคงที่ ) คือการวิเคราะห์โปรแกรมคอมพิวเตอร์ที่ทำโดยไม่ต้องเรียกใช้โปรแกรม ซึ่งแตกต่างจากการวิเคราะห์โปรแกรมแบบไดนามิกซึ่งทำกับโปรแกรมในระหว่างการเรียกใช้ในสภาพแวดล้อมแบบบูรณาการ^{[ 1 ] [ 2 ]}

โดยทั่วไปแล้ว คำนี้มักใช้กับการวิเคราะห์ที่ดำเนินการโดยเครื่องมืออัตโนมัติ ในขณะที่การวิเคราะห์โดยมนุษย์มักเรียกว่า "การทำความเข้าใจโปรแกรม" หรือ " การตรวจสอบโค้ด " ในกรณีหลังนี้ ยังใช้คำ ว่า การตรวจสอบซอฟต์แวร์และการเดินผ่านซอฟต์แวร์ ด้วย ในกรณีส่วนใหญ่ การวิเคราะห์จะดำเนินการกับ โค้ดต้นฉบับของโปรแกรม และในบางกรณี กับ โค้ดออบเจ็กต์ของ โปรแกรม

แนวทางหลักสองแนวทางในการรับรองทรัพยากร ได้แก่ การวิเคราะห์แบบคงที่ (Static Analysis: SA) และ ความซับซ้อนในการคำนวณโดยปริยาย ( Implicit Computational Complexity : ICC) SA มีลักษณะเป็นอัลกอริทึม โดยมุ่งเน้นไปที่ภาษาโปรแกรมที่เลือกอย่างกว้างขวาง และพยายามตรวจสอบด้วยวิธีการทางไวยากรณ์ว่าโปรแกรมที่กำหนดในภาษานั้นสามารถใช้งานได้หรือไม่ ในทางตรงกันข้าม ICC พยายามสร้างภาษาโปรแกรมหรือวิธีการเฉพาะตั้งแต่เริ่มต้น เพื่อกำหนดระดับความซับซ้อน ดังนั้น SA จึงมุ่งเน้นไปที่เวลาในการคอมไพล์ โดยไม่เรียกร้องอะไรจากโปรแกรมเมอร์ ในขณะที่ ICC เป็นระเบียบวินัยในการออกแบบภาษา

ศาสตร์การวิเคราะห์แบบคงที่ (Static Analysis) ไม่ควรสับสนกับศาสตร์การ ตรวจ สอบไวยากรณ์ (Linting ) ซึ่งเป็นกระบวนการตรวจสอบข้อผิดพลาด ด้านรูปแบบการเขียนโค้ด

ความซับซ้อนของการวิเคราะห์ที่ดำเนินการโดยเครื่องมือจะแตกต่างกันไป ตั้งแต่เครื่องมือที่พิจารณาเฉพาะพฤติกรรมของคำสั่งและการประกาศแต่ละรายการ^{[ 4 ]} ไปจนถึงเครื่องมือที่รวม ซอร์สโค้ดทั้งหมดของโปรแกรมไว้ในการวิเคราะห์ การใช้ข้อมูลที่ได้จากการวิเคราะห์จะแตกต่างกันไป ตั้งแต่การเน้นข้อผิดพลาดในการเขียนโค้ดที่อาจเกิดขึ้น (เช่น เครื่องมือ lint ) ไปจนถึงวิธีการที่เป็นทางการที่พิสูจน์คุณสมบัติทางคณิตศาสตร์เกี่ยวกับโปรแกรมที่กำหนด (เช่น พฤติกรรมของโปรแกรมตรงกับข้อกำหนด)

เมตริกซอฟต์แวร์และวิศวกรรมย้อนกลับสามารถอธิบายได้ว่าเป็นรูปแบบของการวิเคราะห์แบบคงที่ การหาเมตริกซอฟต์แวร์และการวิเคราะห์แบบคงที่ถูกนำมาใช้ร่วมกันมากขึ้น โดยเฉพาะอย่างยิ่งในการสร้างระบบฝังตัว โดยการกำหนดสิ่งที่เรียกว่าวัตถุประสงค์ด้านคุณภาพซอฟต์แวร์^{[ 5 ]}

การใช้งานเชิงพาณิชย์ที่เพิ่มขึ้นของการวิเคราะห์แบบคงที่คือการตรวจสอบคุณสมบัติของซอฟต์แวร์ที่ใช้ในระบบคอมพิวเตอร์ที่สำคัญต่อความปลอดภัย และการค้นหา โค้ด ที่อาจ มีช่องโหว่^{[ 6 ]}ตัวอย่างเช่น อุตสาหกรรมต่อไปนี้ได้ระบุการใช้การวิเคราะห์โค้ดแบบคงที่เป็นวิธีการปรับปรุงคุณภาพของซอฟต์แวร์ที่ซับซ้อนและมีความซับซ้อนมากขึ้นเรื่อยๆ:

1. ซอฟต์แวร์ทางการแพทย์ : สำนักงานคณะกรรมการอาหารและยา ของสหรัฐอเมริกา (FDA) ได้ระบุการใช้การวิเคราะห์แบบคงที่สำหรับอุปกรณ์ทางการแพทย์^{[ 7 ]}
2. ซอฟต์แวร์นิวเคลียร์: ในสหราชอาณาจักร สำนักงานกำกับดูแลนิวเคลียร์ (ONR) แนะนำให้ใช้การวิเคราะห์แบบคงที่กับระบบป้องกันเครื่องปฏิกรณ์^{[ 8 ]}
3. ซอฟต์แวร์การบิน (ร่วมกับการวิเคราะห์แบบไดนามิก ) ^{[ 9 ]}
4. ยานยนต์และเครื่องจักร (คุณลักษณะด้านความปลอดภัยเชิงฟังก์ชันเป็นส่วนสำคัญในทุกขั้นตอนการพัฒนาผลิตภัณฑ์ยานยนต์ISO 26262มาตรา 8)

จากการศึกษาในปี 2012 โดย VDC Research พบว่า 28.7% ของวิศวกรซอฟต์แวร์ฝังตัวที่ได้รับการสำรวจใช้เครื่องมือวิเคราะห์แบบคงที่ และ 39.7% คาดว่าจะใช้เครื่องมือเหล่านี้ภายใน 2 ปี^{[ 10 ]} การศึกษาในปี 2010 พบว่า 60% ของนักพัฒนาที่ได้รับการสัมภาษณ์ในโครงการวิจัยของยุโรปใช้เครื่องมือวิเคราะห์แบบคงที่ในตัวของ IDE พื้นฐานอย่างน้อยที่สุด อย่างไรก็ตาม มีเพียงประมาณ 10% เท่านั้นที่ใช้เครื่องมือวิเคราะห์อื่นเพิ่มเติม (และอาจเป็นขั้นสูงกว่า) ^{[ 11 ]}

ในอุตสาหกรรมความปลอดภัยของแอปพลิเคชัน ชื่อการทดสอบความปลอดภัยของแอปพลิเคชันแบบคงที่ (SAST) ก็ถูกนำมาใช้เช่นกัน SAST เป็นส่วนสำคัญของวงจรการพัฒนาความปลอดภัย (SDL) เช่น SDL ที่กำหนดโดย Microsoft ^{[ 12 ]}และเป็นแนวปฏิบัติทั่วไปในบริษัทซอฟต์แวร์^{[ 13 ]}

OMG ( Object Management Group ) ได้เผยแพร่การศึกษาเกี่ยวกับประเภทของการวิเคราะห์ซอฟต์แวร์ที่จำเป็นสำหรับ การวัดและการประเมิน คุณภาพซอฟต์แวร์เอกสารนี้เกี่ยวกับ "วิธีการส่งมอบระบบไอทีที่ยืดหยุ่น ปลอดภัย มีประสิทธิภาพ และเปลี่ยนแปลงได้ง่ายตามคำแนะนำของ CISQ" อธิบายถึงการวิเคราะห์ซอฟต์แวร์สามระดับ^{[ 14 ]}

ระดับหน่วย

การวิเคราะห์ที่เกิดขึ้นภายในโปรแกรมหรือซับรูทีนเฉพาะ โดยไม่เชื่อมโยงกับบริบทของโปรแกรมนั้น

ระดับเทคโนโลยี

การวิเคราะห์ที่คำนึงถึงปฏิสัมพันธ์ระหว่างโปรแกรมย่อยต่างๆ เพื่อให้ได้มุมมองที่ครอบคลุมและมีความหมายมากขึ้นเกี่ยวกับโปรแกรมโดยรวม เพื่อค้นหาปัญหาและหลีกเลี่ยงผลลัพธ์ที่ผิดพลาด อย่าง ชัดเจน

ระดับระบบ

การวิเคราะห์ที่คำนึงถึงปฏิสัมพันธ์ระหว่างโปรแกรมย่อยต่างๆ แต่ไม่จำกัดเฉพาะเทคโนโลยีหรือภาษาโปรแกรมใดภาษาหนึ่ง

สามารถกำหนดระดับการวิเคราะห์ซอฟต์แวร์เพิ่มเติมได้อีกระดับหนึ่ง

ระดับภารกิจ/ธุรกิจ

การวิเคราะห์ที่คำนึงถึงข้อกำหนด กฎ และกระบวนการในระดับธุรกิจ/ภารกิจที่นำมาใช้ภายในระบบซอฟต์แวร์เพื่อการดำเนินงานในฐานะส่วนหนึ่งของกิจกรรมในระดับองค์กรหรือระดับโครงการ/ภารกิจ องค์ประกอบเหล่านี้ถูกนำมาใช้โดยไม่จำกัดเฉพาะเทคโนโลยีหรือภาษาโปรแกรมใดภาษาหนึ่ง และในหลายกรณีมีการกระจายอยู่หลายภาษา แต่จะถูกแยกและวิเคราะห์ในเชิงคงที่เพื่อทำความเข้าใจระบบและเพื่อความมั่นใจในภารกิจ

วิธีการที่เป็นทางการ (Formal methods) คือคำที่ใช้ในการวิเคราะห์ซอฟต์แวร์ (และฮาร์ดแวร์คอมพิวเตอร์ ) ซึ่งผลลัพธ์ได้มาจากการใช้วิธีการทางคณิตศาสตร์ที่เข้มงวดเท่านั้น เทคนิคทางคณิตศาสตร์ที่ใช้ ได้แก่ความหมายเชิงสัญลักษณ์ (denotational semantics ) , ความหมายเชิงสัจพจน์ (axiomatic semantics) , ความหมาย เชิงปฏิบัติการ (operational semantics ) และการตีความเชิงนามธรรม (abstract interpretation )

โดยการลดรูปอย่างตรงไปตรงมาสู่ปัญหาการหยุดทำงานเราสามารถพิสูจน์ได้ว่า (สำหรับภาษาใดๆที่สมบูรณ์แบบตามทฤษฎีบททัวริง ) การค้นหาข้อผิดพลาดขณะทำงานที่เป็นไปได้ทั้งหมดในโปรแกรมใดๆ (หรือโดยทั่วไปแล้ว การละเมิดข้อกำหนดใดๆ เกี่ยวกับผลลัพธ์สุดท้ายของโปรแกรม) นั้นไม่สามารถตัดสินได้ กล่าวคือ ไม่มีวิธีการเชิงกลใดที่สามารถตอบได้อย่างถูกต้องเสมอว่าโปรแกรมใดๆ อาจมีหรือไม่มีข้อผิดพลาดขณะทำงาน ผลลัพธ์นี้มาจากผลงานของChurch , GödelและTuringในช่วงทศวรรษ 1930 (ดู: ปัญหาการหยุดทำงานและทฤษฎีบทของ Rice ) เช่นเดียวกับคำถามที่ไม่สามารถตัดสินได้หลายๆ ข้อ เรายังคงสามารถพยายามให้คำตอบโดยประมาณที่เป็นประโยชน์ได้

เทคนิคการดำเนินการวิเคราะห์สถิตอย่างเป็นทางการบางส่วนได้แก่: ^{[ 15 ]}

• การตีความเชิงนามธรรมคือการจำลองผลกระทบที่แต่ละคำสั่งมีต่อสถานะของเครื่องจักรเชิงนามธรรม (กล่าวคือ 'ดำเนินการ' ซอฟต์แวร์ตามคุณสมบัติทางคณิตศาสตร์ของแต่ละคำสั่งและการประกาศ) เครื่องจักรเชิงนามธรรมนี้ประมาณพฤติกรรมของระบบเกินจริง: ดังนั้นระบบเชิงนามธรรมจึงวิเคราะห์ได้ง่ายขึ้น โดยแลกกับความไม่สมบูรณ์ (ไม่ใช่ทุกคุณสมบัติที่เป็นจริงของระบบดั้งเดิมจะเป็นจริงของระบบเชิงนามธรรม) อย่างไรก็ตาม หากทำอย่างถูกต้อง การตีความเชิงนามธรรมก็ถือว่าสมเหตุสมผล (ทุกคุณสมบัติที่เป็นจริงของระบบเชิงนามธรรมสามารถแมปไปยังคุณสมบัติที่เป็นจริงของระบบดั้งเดิมได้) ^{[ 16 ]}
• การวิเคราะห์การไหลของข้อมูลเป็นเทคนิคที่ใช้โครงสร้างแบบแลตติสในการรวบรวมข้อมูลเกี่ยวกับชุดค่าที่เป็นไปได้
• ตรรกะของ Hoareเป็นระบบที่เป็นทางการที่มีชุดกฎตรรกะสำหรับการให้เหตุผลอย่างเข้มงวดเกี่ยวกับความถูกต้องของโปรแกรมคอมพิวเตอร์มีเครื่องมือสนับสนุนสำหรับภาษาโปรแกรมบางภาษา (เช่นภาษาโปรแกรม SPARK (ส่วนย่อยของAda ) และภาษาสร้างแบบจำลอง Java —JML—โดยใช้ESC/JavaและESC/Java2 ปลั๊กอิน Frama-C WP ( weakest precondition ) สำหรับภาษา C ที่ขยายด้วย ACSL ( ANSI/ISO C Specification Language ))
• การตรวจสอบแบบจำลองพิจารณาระบบที่มีสถานะจำกัดหรือสามารถลดทอนให้เหลือสถานะจำกัดได้โดยการสร้างแบบจำลองนามธรรม
• การประมวลผลเชิงสัญลักษณ์ซึ่งใช้ในการสร้างนิพจน์ทางคณิตศาสตร์ที่แสดงค่าของตัวแปรที่เปลี่ยนแปลงไป ณ จุดต่างๆ ในโค้ด
• การวิเคราะห์การอ้างอิงที่เป็นค่าว่าง

การวิเคราะห์แบบคงที่ที่ขับเคลื่อนด้วยข้อมูลใช้ประโยชน์จากโค้ดเบสจำนวนมากเพื่ออนุมานกฎการเขียนโค้ดและปรับปรุงความแม่นยำของการวิเคราะห์^{[ 17 ] [ 18 ]}ตัวอย่างเช่น สามารถใช้แพ็กเกจโอเพนซอร์ส Java ทั้งหมดที่มีอยู่บนGitHubเพื่อเรียนรู้กลยุทธ์การวิเคราะห์ที่ดี การอนุมานกฎสามารถใช้เทคนิคการเรียนรู้ของเครื่องได้^{[ 19 ]}นอกจากนี้ยังสามารถเรียนรู้จากการแก้ไขและคำเตือนในอดีตจำนวนมากได้อีกด้วย^{[ 17 ]}

เครื่องมือวิเคราะห์แบบคงที่สร้างคำเตือน สำหรับคำเตือนบางประเภท สามารถออกแบบและใช้งาน เทคนิคการ ^{แก้ไข}อัตโนมัติได้ ตัวอย่างเช่น Logozzo และ Ball ได้เสนอการแก้ไขอัตโนมัติสำหรับ C# cccheck [ ^{20 ]}

• Ayewah, Nathaniel; Hovemeyer, David; Morgenthaler, J. David; Penix, John; Pugh, William (2008). "การใช้การวิเคราะห์แบบคงที่เพื่อค้นหาข้อบกพร่อง" IEEE Software . 25 (5): 22– 29. CiteSeerX  10.1.1.187.8985 . doi : 10.1109/MS.2008.130 . S2CID  20646690 .
• Brian Chess, Jacob West (Fortify Software) (2007). การเขียนโปรแกรมที่ปลอดภัยด้วยการวิเคราะห์แบบคงที่ Addison-Wesley. ISBN 978-0-321-42477-8.
• เฟลมมิง นีลสัน; ฮันเน อาร์. นีลสัน; คริส แฮงกิน (10 ธันวาคม 2004). หลักการวิเคราะห์โปรแกรม (ฉบับปี 1999 (แก้ไขเพิ่มเติมปี 2004)). สปริงเกอร์. ISBN 978-3-540-65410-0.
• "การตีความเชิงนามธรรมและการวิเคราะห์เชิงสถิต"งานประชุมวิชาการนานาชาติภาคฤดูหนาวว่าด้วยความหมายและการประยุกต์ใช้ ปี 2003 โดยเดวิด เอ. ชมิดท์