Phương thức và doanh nghiệp chính thức

Question

Vì vậy, ...

Tôi dạy các phương pháp chính thức trong kỹ nghệ phần mềm. Tôi cũng dạy "phương pháp nhanh nhẹn". Hầu hết mọi người dường như nghĩ rằng điều này là mâu thuẫn. Tôi nghĩ nó có ý nghĩa rất nhiều ... Tôi cũng làm việc cho một công ty, nơi mà chúng tôi cần thực sự hoàn thành công việc :) Trong khi tôi có thể áp dụng các điểm kỹ năng kiếm được vào "đặc điểm kỹ thuật" hàng ngày, đồng nghiệp thường chạy trốn khỏi từ "chính thức".

Tôi đã từng nghĩ rằng điều này là do cách nội tại chúng ta học cách lập trình: chúng ta thường được điều khiển để tìm một giải pháp làm việc, không phải để hiểu vấn đề. Sau đó, tôi nghĩ rằng điều này là do thực tế là hầu hết mọi người trong cộng đồng chính thức không phải là kỹ sư, nhưng các nhà toán học hoặc các nhà khoa học máy tính. Ngày nay, tôi tự hỏi liệu đó có phải là vì cộng đồng phương pháp chính thức ẩn đằng sau một số loại luật "obfuscation" để sử dụng tất cả các biểu tượng UNICODE sẵn có, tích cực phát triển các công cụ thô lỗ, không có thẩm mỹ và cười khi đối mặt với các tiêu chuẩn.

Vâng, tôi đã di chuyển từ một "trách họ" tới "đổ lỗi cho chúng tôi" quan điểm ;-)

Vì vậy, câu hỏi của tôi là: Bạn có sử dụng bất kỳ loại phương pháp hình thức trong công ty của bạn? Bạn đã giới thiệu họ chưa, hoặc chúng có phải là điều kiện tiên quyết không? Bạn sử dụng kỹ thuật nào để xóa mờ sương mù của toán học khỏi nỗi sợ hãi của mọi người và kích động họ sử dụng các phương pháp chính thức? Bạn nghĩ gì về các công cụ hiện tại đang thiếu cho việc sử dụng tổng quát hơn?

Answer 1

Chìa khóa để mọi người mua vào bất kỳ phương pháp hoặc phương pháp nào là là chỉ cho họ cách giải quyết các vấn đề mà họ đang gặp phải.Nếu họ có thể nhìn thấy nó sẽ làm cho cuộc sống của họ tốt hơn, bạn có một cơ hội được cải thiện nhiều hơn để giúp họ áp dụng các kỹ thuật.

Và nếu bạn không thể cho họ thấy rằng, có lẽ bạn muốn áp dụng các phương pháp dựa trên triết lý hơn là thực tiễn. Trừ khi những người khác chia sẻ triết lý của bạn thì bạn sẽ không đi đâu cả. Và có lẽ bạn không nên.

Trong nhiều thập kỷ đã có nhiều phương pháp tuyệt vời. Những cái mới hơn luôn luôn giải quyết những thiếu sót của những cái cũ, nhưng các dự án vẫn gặp rắc rối và thất bại. Tại sao? Bởi vì các ngôi sao nhạc rock đưa ra các phương pháp mới là các ngôi sao nhạc rock và đã tạo ra một phương pháp mới một cách chính xác bởi vì chúng hiểu các vấn đề cơ bản và cách áp dụng chúng. Những người đến sau khi có xu hướng mù quáng theo công thức, và nó không hoạt động tốt như vậy.

Vì vậy, tôi nghĩ điều tốt nhất là dạy về các vấn đề cơ bản và sau đó cho thấy các phương pháp khác nhau cố gắng giải quyết những vấn đề đó như thế nào. Sự khác biệt trong các công ty, dự án và nhóm là tuyệt vời đến nỗi không một phương pháp nào có thể được áp dụng thành công cho tất cả các kết hợp. Học cách chọn một công cụ thích hợp và áp dụng nó là rất quan trọng.

Answer 2

Tôi đang tham gia một khóa học về 'Đặc điểm kỹ thuật và xác minh'. Là một phần của cấu trúc khóa học, chúng tôi đang thực hiện các bước sau: 1. Các công cụ học tập như PVS (Hệ thống xác minh mẫu) http://pvs.csl.sri.com/ và SMV (Mô hình hóa và xác minh phần mềm) http://www.cs.cmu.edu/~modelcheck/smv.html 2. Ngoài ra, chúng tôi thực hiện các vụ tai nạn do lỗi phần mềm. . Ví dụ: - Thất bại của Ariane V

Tôi cảm thấy các phương pháp chính thức áp dụng nhiều hơn cho các tình huống mà chi phí thất bại cao hơn chi phí thiết kế. Và có vẻ như apt sử dụng chúng cho các phần mềm được sử dụng trong các hệ thống quan trọng. Tôi đoán nó được sử dụng trong hệ thống điện tử, thiết kế chip vv và ngành công nghiệp ô tô hiện tại cũng đang phác thảo nó thành thực hành.

Answer 3

Tôi đã cố gắng để mọi người nắm bắt các phương pháp đặc điểm kỹ thuật chính thức một vài lần (Z và hợp kim) và đã tạo ra cùng một điều kiện bạn có: Hầu hết mọi người, trong khi cảm thấy rằng họ phục vụ một mục đích hữu ích, rất khó chịu khi sử dụng chúng cho công việc thực tế.

Vui đủ, cùng một người hạnh phúc hơn khi tạo ra các biểu đồ UML vô dụng với số lượng ginormous.

Tôi nghĩ có hai lý do chính cho việc này:.

a) Nhiều nhà phát triển không thoải mái với mức độ trừu tượng theo yêu cầu của một cách tiếp cận chính thức. Thực tế là hầu hết giáo dục toán học cấp nhập cảnh là tất cả các phép tính và không rời rạc-toán học có thể phải làm điều gì đó với điều này.

b.) Các phương thức chính thức yêu cầu thiết kế ở dưới cùng, nơi bạn thiết kế mô hình cốt lõi của mình từ mặt đất và làm cho nó kín khí và sau đó kết nối nó với yêu cầu thực tế của người dùng bằng cách cung cấp giao diện trên đầu. Vì chúng ta có xu hướng có yêu cầu thúc đẩy nỗ lực phát triển, nên cách tiếp cận từ trên xuống cảm thấy tự nhiên hơn mặc dù nó thường dẫn đến các mô hình không nhất quán. Nó giống như trang bị thêm một tầng hầm bên dưới ngôi nhà của bạn sau khi nó đã được xây dựng.

Answer 4

Làm việc với ngành nghề kinh doanh Phát triển CNTT trong doanh nghiệp có nghĩa là phải chuyển giao kiến ​​thức về doanh nghiệp từ những người kinh doanh thực tế thành người đứng đầu nhà phát triển. Trong khi bản thân tôi tìm thấy toán học trừu tượng là một trong những trò tiêu khiển lớn nhất có, đó là một công cụ giao tiếp khủng khiếp. Và thông tin liên lạc là tất cả những gì về nó. Trong khi tôi có thể hình dung được một số thành công thuyết phục người CNTT nắm lấy nhiều ký hiệu trừu tượng hơn, về cơ bản tôi không có cơ hội với những người kinh doanh.

Trong khi có một số lĩnh vực mà tôi có thể thấy vai trò của các phương pháp chính thức trong doanh nghiệp (phần mềm chuyên về toán học và logic, nhu cầu quan trọng đối với các thuộc tính có thể chứng minh được trong phần mềm quan trọng về an toàn) ví dụ làm thế nào để thực hiện một đơn đặt hàng của khách hàng bằng cách phát hành một hoặc nhiều đơn hàng cung cấp cho một tập hợp các nhà cung cấp bên ngoài hoặc bên trong có thể.

Tôi nghĩ ban giám khảo vẫn đang tiếp cận các phương pháp dựa trên mô hình và ngôn ngữ cụ thể của miền. Tôi nghĩ rằng họ sẽ thành công hay thất bại tùy thuộc vào việc họ cung cấp phản hồi nhanh hơn từ CNTT đến mong muốn và nhu cầu của phía doanh nghiệp hay không và liệu họ có cho rằng những người kinh doanh sẽ phải làm bất kỳ nghiên cứu quan trọng nào.

Công nghệ thật dễ dàng. Giao tiếp rất khó. Các phương pháp chính thức có thể giúp chúng ta làm đúng, nhưng những gì tôi thấy không làm gì để giúp chúng ta làm đúng. (Có, đây là những sáo rỗng, nhưng đó là bởi vì chúng không thể tránh khỏi và đau đớn đúng.)

Answer 5

Phương pháp chính thức không có ý nghĩa trong các hệ thống mà chi phí thất bại thấp. Trong một ứng dụng web sản xuất, bạn có nhiều hộp front-end, nhiều hộp back-end, nhiều hộp cơ sở dữ liệu - nếu một chương trình trên bất kỳ một trong số chúng thất bại, đó là một sự kiện không phải. Phần cứng rẻ đến nỗi bạn có thể xây dựng các hệ thống này với chi phí ít hơn so với chi phí chính thức chỉ định tất cả phần mềm của bạn.

Answer 6

Cảm ơn tất cả các đóng góp. Họ rất sâu sắc. Cho phép tôi để ngọn lửa một chút (không mang nó cá nhân, mặc dù :-)

Hầu hết mọi người dường như nghĩ rằng phương pháp chính thức chỉ là về xác minh chương trình. Hoặc các hệ thống quan trọng. Điều này có thể đúng nếu chúng tôi theo đuổi những câu đố cuối cùng: để chứng minh chúng tôi đang làm đúng chương trình (v.s. xác nhận, yêu cầu, như một người đóng góp cho biết, nếu chúng tôi đang làm đúng chương trình).

Nhưng hãy xem xét công cụ tìm/kiểm tra mô hình, chẳng hạn như Hợp kim.Học cách sử dụng một công cụ như thế này sẽ mất rất nhiều thời gian cho bất kỳ ai sử dụng UML và OO. Tuy nhiên, nó có thể cung cấp cho bạn cái nhìn sâu sắc ngay lập tức về mô hình của bạn. Nó thường mất không quá 10 phút để tìm một ví dụ phản đối trên một tập hợp con nhỏ đủ của mô hình của một người cố gắng sử dụng (và bao gồm mô tả mô hình trong Hợp kim ở nơi đầu tiên).

Lấy yêu cầu kỹ thuật làm ví dụ. Một thường vẽ rất nhiều UML. Tuy nhiên, rất ít người sử dụng OCL và nhiều quy tắc kinh doanh được chú thích không chính thức bằng ngôn ngữ tự nhiên. Tại sao? Hạn chế thời gian?

Bây giờ, hãy xem xét thực tế là đa số chỉ sử dụng cảm giác ruột của mình để chứng minh rằng mô hình là thỏa đáng. Một lần nữa, tại sao? Tôi có thể mất cùng một lượng thời gian (có lẽ thậm chí còn ít hơn, vì tôi không cần phải quan tâm đến việc vẽ thẩm mỹ) để viết mô hình đó trong Hợp kim, và chỉ kiểm tra sự thỏa mãn? Và tôi cần loại toán học gì bây giờ? "Predicates"? Tên ưa thích cho IF và booleans ;-) Định lượng? Tên lạ mắt cho ForEachs() ...

Còn hệ thống thông tin lớn thì sao? Họ không cần phải quan trọng ... Chỉ cần cố gắng phân tích trong đầu của bạn một sơ đồ khái niệm (không thực hiện!) Với hơn 600 lớp. Tôi thấy nhiều người đập đầu vào tường với những sai lầm về mô hình dễ làm bởi vì họ bỏ lỡ một số ràng buộc, hoặc mô hình cho phép những điều ngu xuẩn xảy ra.

Thực tế là, người ta không cần sử dụng phương pháp tiếp cận chính thức từ đầu đến đuôi. Cấp, tôi có thể chứng minh một ứng dụng toàn bộ trong Coq, và xác nhận rằng nó là 100% phù hợp với một số đặc điểm kỹ thuật. Đây có thể là cách tiếp cận Nhà khoa học máy tính/Toán học.

Tuy nhiên, với một triết lý GTD, tại sao tôi không thể ủy nhiệm một số nhiệm vụ cho máy tính và cho phép nó giúp cải thiện sự phát triển của tôi? Nó thực sự là vấn đề "thời gian", hoặc thiếu đơn giản, kỹ năng kỹ thuật và sẽ học/inovate?