Special Topic in Software Engineering (¼ÒÇÁÆ®¿þ¾î°øÇРƯ°­)
- Software Quality      
(2012 Spring for graduate students)
¡¡

Syllabus

This course introduces theoretical background and recent techniques on software quality and safety analysis.
Each student selects one key paper about software quality and makes a series of presentations in advance.
He (She) will also propose a research plan at the end of the semester.

Prerequisite: All student are strongly recommended to take the "Advanced Software Engineering - Formal Methods" course prior to taking this course.


Text & Lecture Notes:
 - by Nancy G. Leveson  - by Daniel Jackson, et. al.   - by Nancy G. Leveson

   - SAFEWARE
   - Software for Dependable Systems (a public online file)
   - Engineering a Safer World (a public draft)



Grading plan:
    - Presentation : 70%
    - Proposal : 30%



2012.02.06 :  ù ¼ö¾÷Àº 03.02(±Ý) 15:00~18:00 (1207È£) ÀÔ´Ï´Ù.
2012.02.24 :  °¡´ÉÇÏ¸é ´ëÇпø "°í±Þ¼ÒÇÁÆ®¿þ¾î°øÇÐ" ¼ö°­ÇÑ Çлýµé¸¸ ½ÅûÇϼ¼¿ä. ¾Æ½±Áö¸¸, ¼ö¾÷ µû¶ó ¿À½Ã±â°¡ ½±Áö ¾Ê½À´Ï´Ù.
2012.03.12 :  Ãß°¡/È®Àå ³í¹®À» ¹ßÇ¥ÇÏ½Ç ¶§´Â, ¹ßÇ¥ÀÚ·á¿Í ÇÔ²² ³í¹® lists ¹× filesµµ ÇÔ²² º¸³» ÁÖ¼¼¿ä.
2012.03.20 :  ¹ßÇ¥ ½ºÄÉÁì¿¡ ¾à°£ÀÇ º¯µ¿ÀÌ ÀÖ½À´Ï´Ù. È®ÀÎÇϼ¼¿ä.
2012.03.25 :  03.30 ¼ö¾÷ ÈÞ°­ÇÕ´Ï´Ù.
2012.04.14 :  2012.04.20(±Ý) Á¤»ó¼ö¾÷ ÇÕ´Ï´Ù.
2012.04.16 :  2012.04.21(Åä) 10:00 ~ 12:00 907È£ "º¸°­"ÇÕ´Ï´Ù. ³»¿ë: C1(À̵¿¾Æ)  C2(À±»óÇö) - ¿øÇϽô ºÐ¸¸ Âü¼®Çϼŵµ µË´Ï´Ù ^^
¡¡

¡¡

Schedule

Week Date Lecture
1 03.02  Course Introduction, 5(À̼±ÈÖ)
2 03.09  A(À̵¿¾Æ) ,  6(±è¼±¸ð)
3 03.16  B(À±»óÇö) , C(¼ÕÇö½Â)
4 03.23  H(Á¶À翬) , 1(À̼±ÈÖ) , 2(ÀÌÁ¾ÈÆ)
5 03.30  ÈÞ°­
6 04.06  I(ÀÌÁ¾ÈÆ) , E(Á¶À翬) , 9(Àº¾Öõ)
7 04.13  C1(À̵¿¾Æ) , C1(À±»óÇö) , 10(±èÀǼ·)
8 04.20  12(±è¼±¸ð) , 8(ÇÑ»óÇö) , D(¼ÕÇö½Â)
9 04.27  L(±èÀǼ·) , 4(Àå¹ü¼®)
10 05.04  15(±èÁÖÈ£) , 11(±èÁ¾¼­) , È®Àå³í¹®(À̵¿¾Æ)
11 05.11  È®Àå³í¹®(À±»óÇö) , K(ÇãÁÖ½Â) , 3(±èÀǼ·)
12 05.18  J(ÇãÁÖ½Â) ,  G(À̼±ÈÖ) ,  È®Àå³í¹®(¼ÕÇö½Â) , 14(°í¼ºÇÐ)
13 05.25  ³í¹®¿¬±¸ °èȹ in depth (À̵¿¾Æ)
 È®Àå³í¹® ¹ßÇ¥ (Àº¾Öõ , ÇÑ»óÇö , Àå¹ü¼® , ±èÁ¾¼­)
14 06.01  È®Àå³í¹® ¹ßÇ¥ (±èÁÖÈ£ , ±è¼±¸ð , ÇãÁֽ , °í¼ºÇÐ)
15 06.08  ÈÞ°­ (ICSE 2012 Âü°¡)
16 06.15  ³í¹®¿¬±¸ °èȹ in depth (À±»óÇö)
 ³í¹®¿¬±¸ °èȹ (ÀÌÁ¾ÈÆ, Á¶À翬, ±èÀǼ·, À̼±ÈÖ)

¡¡

¡¡

Key Papers

À̸§ ³í¹®¹ßÇ¥ #1 ¿¬±¸°èȹ Áß°£¹ßÇ¥ ³í¹®¹ßÇ¥ #2 - È®Àå³í¹® ¿¬±¸³í¹® ÇÁ·ÎÆ÷Àý
À̵¿¾Æ A , C1(4Àå)
À±»óÇö B , C1(8,9Àå) , F
ÀÌÁ¾ÈÆ I , 2 N/A
Á¶À翬 E , H N/A
±èÀǼ· L , 10 , 3 N/A N/A
À̼±ÈÖ G , 1 , 7 , 5 N/A N/A
¼ÕÇö½Â C , D
±èÁ¾¼­ 11
Àå¹ü¼® 4
ÇÑ»óÇö 8
ÇãÁֽ J , K
Àº¾Öõ 9
°í¼ºÇÐ 14
±èÁÖÈ£ 15
±è¼±¸ð 6 , 12

¡¡

ºÐ¾ß ÁÖ¿ä ³í¹®


Advanced Topics on Formal Methods
¡¡
 Dependability Arguments  A.  Software for Dependable System: Sufficient Evident? National Research Council, 2007 (À̵¿¾Æ)
   - A.1 Engineering Software Systems for Customer Acceptance, TR (À̵¿¾Æ)
   - A.2
 B.  A Direct Path to Dependable Software, Communication of the ACM, 2009 (À±»óÇö)
   - B.1  Assurance based Development of Critical Systems, in DSN, 2007
   - B.2  The Goal Structuring Notation - A Safety Argument Notation, in DSN, 2004
   - B.3  Using Fault Modeling in Safety Cases, in ISSRE, 2008
   - B.4  A Framework for Dependability Analysis of Software Systems with Trusted Bases, Master's thesis, MIT, 2010
   - B.5  A Systematic Approach to Safety Case Maintenance, RESS, 2001
   - B.6  Safety Case Construction and Reuse using Patterns, in SAFECOMP, 1997.
   - B.7  Architectural considerations in the certification of modular systems, in SAFECOMP, 2002
 Accident Model  C.  A New Accident Model for Engineering Safer Systems, Safety Science, 2004 (¼ÕÇö½Â)
   - C.1 Engineering a Safer World (À̵¿¾Æ) (À±»óÇö)
   - C.2 Application of a Safety-Driven Design Methodology to an Outer Planet Exploration Mission, in AC 2008
   - C.3 A System-Theoretic Hazard Analysis Methodology for a Non-Advocate Safety Assessment of the Ballistic
          Missile Defense System, in AIAA MSC 2006
   - C.4 STAMP-based analysis on the railway accident and accident spreading, SS 2010 (À̵¿¾Æ)
 Safety vs. Security  D.  The SEMA Referential Framework: Avoiding Ambiguities in the Terms "Security" and "Safety", IJCIP, 2010
   - D.1
   - D.2 
 Requirements Elicitation  E.  From Safety Analysis to Software Requirements, IEEE TSE, 2002 (Á¶À翬)
   - E.1
 F.  Deriving Specifications from Requirements: An example, in ICSE, 1995
   - F.1
   - F.2
 Safety Analysis  G.  Integrating Safety Analysis Techniques, Supporting Identification of Common Cause Failures, PhD Thesis 2000
 H.  Temporal Fault Trees, IST, 2002
   - H.1 A Model-Oriented Approach to Safety Analysis using Fault Trees and a Support System, JSS 1996
   - H.2 TLA in Pictures, IEEE TSE 1995
 Safety-focused Development  I. Analysis and Synthesis of the Behaviour of Complex Programmable Electronic Systems in Conditions of Failure,
    RESS, 2001
   - I.1
   - I.2
   - I.3
 J. A Safety-Focus Verification using Software Fault Trees, FGCS, 2011 (ÇãÁÖ½Â)
 K. A Software Quality Assessment Framework for Dependable Systems, FSE 2012 draft (ÇãÁÖ½Â)
 L. Formal Modeling and Verification of Safety-Critical Software, IEEE Software, 2009 (±èÀǼ·)
   - L.1 SCADE
   - L.2
   - L.3
 
Fundamentals of Formal Methods
¡¡
 Alloy  1. http://alloy.mit.edu/alloy/ (À̼±ÈÖ)
 MSC  2. Synthesis of Behavioral Models from Scenarios, IEEE TSE 2003
 SCR  3. Specifying software requirements for Complex Systems: New Techniques and Their Application IEEE TSE 1980 (±èÀǼ·)
 4. Software Cost Reduction, TR (Àå¹ü¼®)
 Statecharts  5. On Visual Formalisms, Communication of the ACM 1989 (À̼±ÈÖ)
 HyTech  6. HYTECH: a model checker for hybrid systems, STTT 1997 (±è¼±¸ð)
 RSML  7. Completeness and consistency in hierarchical state-based requirements, IEEE TSE 1996
 Model Checking  8. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM TPLS 1986 (ÇÑ»óÇö)
 SPIN  9. The Model Checker Spin, IEEE TSE 1997 (Àº¾Öõ)
 Testing  10. Software Unit Test Coverage and Adequacy, ACM Computing Surveys 1997 (±èÀǼ·)
 Hybrid System  11. System Theoretic Formalisms for Combined Discrete-Continuous System Simulation, IJGS 1991 (±èÁ¾¼­)
 12. Hierarchical Modeling and Analysis of Embedded Systems, P. IEEE 2003 (±è¼±¸ð)
 Temporal Logic  13. Temporal and Modal Logic, in Handbook of TCS 1990
 Applications of Verification

 14. Formal Verification of an OS Kernel, Communications of the ACM 2010 (°í¼ºÇÐ)
 15. Formal Verification on Multitasking Applications based on Timed Automata Model, Real-Time Systems 2008 (±èÁÖÈ£)
 16. Early Verification and Validation of Mission Critical Systems, FMSD 2007
 Software Architecture  17. Software Architecture Reconstruction: A Process-Oriented Taxonomy, IEEE TSE 2009

¡¡

¡¡